2
$\begingroup$

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.

$\endgroup$

1 Answer 1

5
$\begingroup$

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).

$\endgroup$
21
  • $\begingroup$ Thank you, this makes explicit the uneasy feeling I had about this argument. $\endgroup$
    – Alec Rhea
    Mar 3, 2022 at 14:52
  • $\begingroup$ 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? $\endgroup$
    – Alec Rhea
    Mar 5, 2022 at 5:36
  • $\begingroup$ 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. $\endgroup$ Mar 5, 2022 at 8:54
  • $\begingroup$ A protocategory is more or less an archaic set-theoretic way to approximate the natural dependently typed definition. $\endgroup$ Mar 5, 2022 at 8:55
  • $\begingroup$ 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. $\endgroup$
    – Alec Rhea
    Mar 5, 2022 at 14:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.