Uniqueness of comparison functors

Question

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.

Answer 1

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