2

Given an adjunction $F\dashv G:\mathcal{C}\rightleftarrows\mathcal{D}$ with unit $\eta$ and counit $\epsilon$, we naturally have a monad $(G\circ F,\eta,G\epsilon_F)$ on $\mathcal{C}$ and a comparison functor $K:\mathcal{D}\to\mathcal{C}^{G\circ F}$ (where $\mathcal{C}^{G\circ F}$ is the E-M category of this monad) given by $$K(D)=\big(G(D),G(\epsilon_D)\big),$$ $$K(f:D\to D')=G(f).$$ This functor is unique satisfying $$?\circ K=G, \hspace{10mm} K\circ F=\widehat {G\circ F},$$ as shown in e.g. Mac Lane, p.142.

It seems like the proof that this functor is unique satisfying these equations should be way easier than it is in Mac Lane. He uses the fact that $$(1_\mathcal{C},K):F\dashv G:\mathcal{C}\rightleftarrows\mathcal{D}\longrightarrow\widehat{G\circ F}\dashv\ ?:\mathcal{C}\rightleftarrows\mathcal{C}^{G\circ F}$$ is a morphism of adjunctions by the above equations and the fact that both adjunctions have the same unit, then looks at the equivalent counit condition for morphisms of adjunctions to conclude that any other functor $K':\mathcal{D}\to\mathcal{C}^{G\circ F}$ satisfying $?\circ K'=G$ and $K'\circ F=\widehat{G\circ F}$ agrees with $K$ on structure maps.

Why is this not immediately true since $K$ and $K'$ agree on arrows?

In particular, any two functors $F,G:\mathcal{A}\rightrightarrows\mathcal{B}$ which agree on arrows immediately agree on objects since $$F(X)=F(dom(1_X))=dom(F(1_X))=dom(G(1_X))=G(dom(1_X))=G(X),$$ and the equation $?\circ K=G=\ ?\circ K'$ tells us that $K$ and $K'$ agree on arrows -- they're both just $G$ on arrows since $?$ leaves arrows unchanged.

Can we just repeat the above argument with $F=K$ and $G=K'$ and be done?

I can't find anything wrong with this reasoning, but I suspect Mac Lane would have taken this route if it worked.

Alec Rhea
  • 9,009

1 Answers1

6

Your argument that any two functors that agree on arrows must agree on objects depends on assuming that the homsets of a category are disjoint, so that every arrow has exactly one domain and codomain. But even if the homsets of $\mathcal{C}$ are disjoint, the homsets of $\mathcal{C}^{G\circ F}$ won't generally be: a given arrow $f:X\to Y$ in $\mathcal{C}$ can be a $(G\circ F)$-algebra morphism between more than one pair of $(G\circ F)$-algebra structures on $X$ and $Y$.

In general, it's dangerous to try to do category theory treating the arrows in a non-dependently typed manner. In particular, it doesn't really make sense to ask whether two arrows are equal unless you already know that their domains and codomains are equal (so that they have the same type).

Mike Shulman
  • 65,064
  • Thank you, this makes explicit the uneasy feeling I had about this argument. – Alec Rhea Mar 03 '22 at 14:52
  • But wait, how does this square with the fact that a category has a domain and codomain function, sending each arrow to ‘it’s domain and codomain’? Is the EM category a protocategory and not a category, and if so is there a way to canonically obtain a category out of a protocategory? – Alec Rhea Mar 05 '22 at 05:36
  • A category only has a domain and codomain function when you use the one-collection-of-morphisms definition of category. But in practice, such as when defining the EM category, we generally use the dependently typed definition of category. It's easy to make the latter definition into the former by taking a disjoint union of the homsets, but there's rarely any point to that. – Mike Shulman Mar 05 '22 at 08:54
  • 1
    A protocategory is more or less an archaic set-theoretic way to approximate the natural dependently typed definition. – Mike Shulman Mar 05 '22 at 08:55
  • Ah, so we really do have to think about there being a proper class of copies of each function in ${\bf Set}$ since the the codomain of each function has a proper class of supersets; I find that hilarious. – Alec Rhea Mar 05 '22 at 14:30
  • I would say the correct definition of "a function" includes its domain and codomain. Otherwise what is its type? It's only in the weird world where everything is unnaturally encoded in terms of a global membership predicate like that of ZFC that you can even talk about an abstract "set of ordered pairs" without first specifying what sets the components of those pairs are to be drawn from. (-:O – Mike Shulman Mar 05 '22 at 17:33
  • As much as I've been keenly awaiting the day that type theory feels like a more natural foundation than set theory, constantly expecting it around each new bend I take deeper into category theory, I am still left with the feeling that I would only prefer type theory if I were a computer or a human who needed to think similarly to a computer. There is something about set theory that captures my nascent intuition for 'how things should be in the multiverse' in a way that feels almost like religion; I do still eagerly await the day type theory feels the same. – Alec Rhea Mar 07 '22 at 02:01
  • And it doesn't help that thinking set-theoretically is what led you to make the mistake in this question, while thinking type-theoretically it wouldn't even have entered your awareness? – Mike Shulman Mar 07 '22 at 04:53
  • It indicates that I wasn't listening hard enough to my intuition for what the set-theoretical universe looks like; I've idly considered the fact that the ordered pairs definition of a function is somewhat ambiguous on what its codomain is, and I've idly considered that there are a proper class of options for any function, but I never put 2 and 2 together to realize that we effectively have a proper class of copies of each function. If I had walked out the few extra steps the error in my intuition would have become clear with no need for types, and (cont.) – Alec Rhea Mar 07 '22 at 06:31
  • there are still questions that have occurred to me thinking set-theoretically about category theory that I don't even see how to pose type theoretically, let alone answer them. – Alec Rhea Mar 07 '22 at 06:32
  • Yes, you can avoid making type errors when you program with assembly language, but it's much easier to avoid them if you use a language whose compiler will catch them for you. – Mike Shulman Mar 07 '22 at 07:32
  • What makes you think there would be any difficulty in posing those questions type-theoretically? – Mike Shulman Mar 07 '22 at 07:33
  • Touché on the programming language metaphor (although we are now humans thinking like computers as I feared); more seriously, do you really feel like material set theories with a global membership predicate are as difficult to work with as programming in compiler would be? I find the ' disorganized mélange of concepts' immediately present in a material set theory to be a boon in the sense that I can 'see how to define what I want', and categories in turn arrange the mélange into a beautiful hierarchy. – Alec Rhea Mar 07 '22 at 08:55
  • Probably nothing but ignorance on my part would prevent me from posing them, but I do feel (perhaps due to more ignorance) that those notions are more thoroughly explored and cared about by the set theory community -- I have never seen a question posed about forcing from a type theorist, but a brief googling did turn up some material so maybe I'm just wrong. – Alec Rhea Mar 07 '22 at 08:57
  • Granted, the difference between type theory and material set theory is not as extreme as that between high-level programming languages and assembler, although part of that is because in practice mathematicians don't usually actually use material set theory but rather an informal type-theory-like layer built on top of it. But it matters, not just to rule out questions like this, but especially when teaching students who haven't yet internalized that informal layer. – Mike Shulman Mar 07 '22 at 15:59
  • Of course questions about forcing are more thoroughly explored and cared about by the set theory community. Questions about group theory are also more thoroughly explored and cared about by the group theory community, etc. etc. That doesn't have anything to do with whether the questions can be formulated in a type-theoretic foundation. – Mike Shulman Mar 07 '22 at 16:01
  • To further beat a dead horse: how does this square with Peter's answer asserting an equivalence between the categories of categories with disjoint hom-sets and the category of categories with possibly non-disjoint hom-sets (also mentioned on the nlab)? Does my argument work 'up to equivalence', so my intuition is already correct 'up to equivalence'? – Alec Rhea Mar 11 '22 at 10:18
  • I consider forcing (and related notions of 'moving between universes') more fundamental to 'how the multiverse is' in that pseudoreligious sense than things studied by group theorists etc., though, and so gain more by viewing things set theoretically than I would viewing them e.g. group theoretically. – Alec Rhea Mar 11 '22 at 10:19
  • You're free to believe forcing to be "more fundamental" than group theory. My point was just that the fact that questions about forcing phrased in categorical language haven't been asked by non-set-theorists says no more about whether those questions can be posed in the correct dependently typed language of category theory than the fact that questions about group theory phrased in categorical language haven't been asked by non-group-theorists says anything analogous about those questions. – Mike Shulman Mar 11 '22 at 16:00
  • Category theory is (among other things) a language for talking about questions in other subjects, applicable to set theory as well as to group theory. This doesn't mean that all questions about set theory can be phrased using category theory; but when you do use that language you should use it correctly, regardless of the subject. – Mike Shulman Mar 11 '22 at 16:01
  • If you're referring to your construction of the functor Force in that other question, it's already written (like nearly all mathematics) in "informal dependent type theory", so there's nothing to worry about: of course it's insensitive to how you define categories. – Mike Shulman Mar 11 '22 at 16:03