I'm trying to understand proposition 3.' HoCA (vol. I).

Proposition 3.4.2 Consider a functor $F\colon \mathcal A \to \mathcal B$ with both a left adjoint functor $G$ and a right adjoint functor $H$. If functor is full and faithful, si is the other adjoint functor.

There are some minor typos in the proof, but they're not a big deal.

Borceux calls $\epsilon \colon GF \Rightarrow 1_{\mathcal A}$, $\eta\colon 1_{\mathcal B} \Rightarrow FG$ and $\alpha \colon FH \Rightarrow 1_{\mathcal B}$, $\beta\colon 1_{\mathcal A} \Rightarrow HF$ the counits and units of the adjuctions.

By duality, it is enough to prove, wlog, that if H is fully faithful then the same holds for G. Further, this statement is equivalent (by proposition 3.4.1) to say that $\eta$ is iso whenever $\alpha$ is.

The claim is that

$\alpha \circ (1_F *\epsilon * 1_H) \circ (1_{FG}*\alpha^{-1}) = \eta^{-1}$.

By the naturality of $eta$,

$\alpha \circ (1_F *\epsilon * 1_H) \circ (1_{FG}*\alpha^{-1}) \circ \eta = \alpha \circ (1_F *\epsilon * 1_H) \circ (\eta*1_{FH})\circ \alpha^{-1}.$

The trangular equality, i.e., $(1_F *\epsilon) \circ (\eta*1_{F}) = 1_{\mathcal F}$ (thus, in particular $(1_F *\epsilon *1_H) \circ (\eta*1_{FH}) = 1_{\mathcal FH}$), gives us

$alpha \circ \alpha^{-1} = 1_{\mathcal B}$.

On the other hand, first note that the triangular equality

$(\alpha *1_F)\circ (1_F * \beta) = 1_F$

implies that $1_F* \beta = (\alpha *1_F)^{-1}\quad(\heartsuit)$.

Now consider

$\star = \eta\circ \alpha \circ (1_F *\epsilon * 1_H) \circ (1_{FG}*\alpha^{-1})$

$\star = (\text{by naturality of }\alpha) = (\alpha*1_{FG})\circ (1_{FH}*\eta) \circ (1_F *\epsilon * 1_H) \circ (1_{FG}*\alpha^{-1})$

$\star = (\text{by naturality of }1_F *\epsilon * 1_H) = (\alpha*1_{FG})\circ (1_F *\epsilon * 1_{HFG})\circ (1_{FGFH}*\eta) \circ (1_{FG}*\alpha^{-1})$

$\star = (\text{by naturality of }1_{FG}*\alpha^{-1}) = (\alpha*1_{FG})\circ (1_F *\epsilon * 1_{HFG})\circ (1_{FG}*\alpha^{-1}*1_{FG}) \circ (1_{FG} *\eta)$

Using $(\heartsuit)$, $\star$ is thus equal to

$(\alpha *1_{FG}) \circ (1_F*\epsilon *1_{HFG}) \circ (1_{FGF}*\beta *1_G) \circ (1_{FG}*\eta)$.

(Borceux writes

$(1_{FG}*\alpha) \circ (1_F*\epsilon *1_{HFG}) \circ (1_{FGF}*\beta *1_G) \circ (1_{FG}*\eta)$,

but I think there's a small typo).

The next (and last) equality is

$(\alpha *1_{FG}) \circ (1_F*\epsilon *1_{HFG}) \circ (1_{FGF}*\beta *1_G) \circ (1_{FG}*\eta) = (1_F*1_G)\circ (1_F*1_G)$.

Where does this equality come from?

Aside question. Proving all these last equalities I've realized that, if $A$ is a category, $F, G\colon A \to A$ are endofunctors, $\alpha\colon F\to 1_A$, $\beta\colon 1_A \to G$ are natural transformations, then

$\beta \circ \alpha = (\alpha *1_G)\circ (1_F *\beta)$.

I suppose that, maybe using the interchange law for 2-cells and doing some checks, lemma general enough to prove immediately the equalities in the last part of the proof.

  • 2
    $\begingroup$ It's a good idea to at least explain what the proposition is (as well as an outline of the argument up to this point), for the benefit of everyone who does not have that book at hand. $\endgroup$ May 16 '13 at 23:01
  • 1
    $\begingroup$ Presumably $\eta$ and $\epsilon$ are adjunction unit and counit and $\alpha$ and $\beta$ are mutually inverse, or something like that? Then just push $\epsilon$ past $\beta$ using naturality. $\endgroup$
    – Zhen Lin
    May 16 '13 at 23:04
  • $\begingroup$ I have improved the question with some more background. @ZhenLin, do you mean $(1_F*\epsilon *1_{HFG}) \circ (1_{FGF}*\beta *1_G) = (1_F * \beta * 1_G)\circ (1_F * \epsilon 1_G)$? $\endgroup$ May 16 '13 at 23:51

I will use the same notation. By naturality, $$(1_F * \epsilon * 1_{H F G}) \circ (1_{F G F} * \beta * 1_G) = (1_F * \beta * 1_G) \circ (1_F * \epsilon * 1_G)$$ and so $$(\alpha * 1_{F G}) \circ (1_F * \epsilon * 1_{H F G}) \circ (1_{F G F} * \beta * 1_G) \circ (1_{F G} * \eta)$$ is equal to $$(\alpha * 1_{F G}) \circ (1_F * \beta * 1_G) \circ (1_F * \epsilon * 1_G) \circ (1_{F G} * \eta)$$ which by the triangle identities is just $1_{F G}$.

  • $\begingroup$ Many thanks! Now I've got it. $\endgroup$ May 17 '13 at 9:23

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.