Proposition 9.6.2.1.2 (011T): Properties of Full Functors

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

Let $F\colon \mathcal{C}\to \mathcal{D}$ and $G\colon \mathcal{D}\to \mathcal{E}$ be functors.

Interaction With Composition. If $F$ and $G$ are full, then so is $G\circ F$.
Interaction With Postcomposition I. If $F$ is full, then the postcomposition functor
\[ F_{*} \colon \mathsf{Fun}\webleft (\mathcal{X},\mathcal{C}\webright ) \to \mathsf{Fun}\webleft (\mathcal{X},\mathcal{D}\webright ) \]

can fail to be full.
Interaction With Postcomposition II. If, for each $\mathcal{X}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$, the postcomposition functor
\[ F_{*} \colon \mathsf{Fun}\webleft (\mathcal{X},\mathcal{C}\webright ) \to \mathsf{Fun}\webleft (\mathcal{X},\mathcal{D}\webright ) \]

is full, then $F$ is also full.
Interaction With Precomposition I. If $F$ is full, then the precomposition functor
\[ F^{*} \colon \mathsf{Fun}\webleft (\mathcal{D},\mathcal{X}\webright ) \to \mathsf{Fun}\webleft (\mathcal{C},\mathcal{X}\webright ) \]

can fail to be full.
Interaction With Precomposition II. If, for each $\mathcal{X}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$, the precomposition functor
\[ F^{*} \colon \mathsf{Fun}\webleft (\mathcal{D},\mathcal{X}\webright ) \to \mathsf{Fun}\webleft (\mathcal{C},\mathcal{X}\webright ) \]

is full, then $F$ can fail to be full.
Interaction With Precomposition III. If $F$ is essentially surjective and full, then the precomposition functor
\[ F^{*} \colon \mathsf{Fun}\webleft (\mathcal{D},\mathcal{X}\webright ) \to \mathsf{Fun}\webleft (\mathcal{C},\mathcal{X}\webright ) \]

is full (and also faithful by Item 4 of Proposition 9.6.1.1.2).
Interaction With Precomposition IV. The following conditions are equivalent:
1. For each $\mathcal{X}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$, the precomposition functor
  \[ F^{*} \colon \mathsf{Fun}\webleft (\mathcal{D},\mathcal{X}\webright ) \to \mathsf{Fun}\webleft (\mathcal{C},\mathcal{X}\webright ) \]
  
  is full.
2. The functor $F\colon \mathcal{C}\to \mathcal{D}$ is a corepresentably full morphism in $\mathsf{Cats}_{\mathsf{2}}$ in the sense of Chapter 11: Graphs, Definition 11.2.1.1.1.
3. The components
  \[ \eta _{G}\colon G\Longrightarrow \text{Ran}_{F}\webleft (G\circ F\webright ) \]
  
  of the unit
  
  \[ \eta \colon \text{id}_{\mathsf{Fun}\webleft (\mathcal{D},\mathcal{X}\webright )}\Longrightarrow \text{Ran}_{F}\circ F^{*} \]
  
  of the adjunction $F^{*}\dashv \text{Ran}_{F}$ are all retractions/split epimorphisms.
4. The components
  \[ \epsilon _{G}\colon \text{Lan}_{F}\webleft (G\circ F\webright )\Longrightarrow G \]
  
  of the counit
  
  \[ \epsilon \colon \text{Lan}_{F}\circ F^{*}\Longrightarrow \text{id}_{\mathsf{Fun}\webleft (\mathcal{D},\mathcal{X}\webright )} \]
  
  of the adjunction $\text{Lan}_{F}\dashv F^{*}$ are all sections/split monomorphisms.
5. For each $B\in \text{Obj}\webleft (\mathcal{D}\webright )$, there exist:
  - An object $A_{B}$ of $\mathcal{C}$;
  - A morphism $s_{B}\colon B\to F\webleft (A_{B}\webright )$ of $\mathcal{D}$;
  - A morphism $r_{B}\colon F\webleft (A_{B}\webright )\to B$ of $\mathcal{D}$;
  satisfying the following condition:
  - For each $A\in \text{Obj}\webleft (\mathcal{C}\webright )$ and each pair of morphisms
    \begin{align*} r & \colon F\webleft (A\webright ) \to B,\\ s & \colon B \to F\webleft (A\webright ) \end{align*}
    
    of $\mathcal{D}$, we have
    
    \[ \webleft [\webleft (A_{B},s_{B},r_{B}\webright )\webright ]=\webleft [\webleft (A,s,r\circ s_{B}\circ r_{B}\webright )\webright ] \]
    
    in $\int ^{A\in \mathcal{C}}h^{B'}_{F_{A}}\times h^{F_{A}}_{B}$.

Item 1: Interaction With Composition

Since the map

\[ \webleft (G\circ F\webright )_{A,B} \colon \textup{Hom}_{\mathcal{C}}\webleft (A,B\webright ) \to \textup{Hom}_{\mathcal{D}}\webleft (G_{F_{A}},G_{F_{B}}\webright ), \]

defined as the composition

\[ \textup{Hom}_{\mathcal{C}}\webleft (A,B\webright )\xrightarrow {F_{A,B}}\textup{Hom}_{\mathcal{D}}\webleft (F_{A},F_{B}\webright )\xrightarrow {G_{F\webleft (A\webright ),F\webleft (B\webright )}}\textup{Hom}_{\mathcal{D}}\webleft (G_{F_{A}},G_{F_{B}}\webright ), \]

is a composition of surjective functions, it follows from that it is also surjective. Therefore $G\circ F$ is full.

Item 2: Interaction With Postcomposition I

We follow the proof (completely formalised in cubical Agda!) given by Naïm Camille Favier in [Favier, Postcompose Not Full]. Let $\mathcal{C}$ be the category where:

Objects. We have $\text{Obj}\webleft (\mathcal{C}\webright )=\webleft\{ A,B\webright\} $.
Morphisms. We have
\begin{align*} \textup{Hom}_{\mathcal{C}}\webleft (A,A\webright ) & = \webleft\{ e_{A},\text{id}_{A}\webright\} ,\\ \textup{Hom}_{\mathcal{C}}\webleft (B,B\webright ) & = \webleft\{ e_{B},\text{id}_{B}\webright\} ,\\ \textup{Hom}_{\mathcal{C}}\webleft (A,B\webright ) & = \webleft\{ f,g\webright\} ,\\ \textup{Hom}_{\mathcal{C}}\webleft (B,A\webright ) & = \text{Ø}. \end{align*}
Composition. The nontrivial compositions in $\mathcal{C}$ are the following:

\[ \begin{aligned} e_{A}\circ e_{A} & = \text{id}_{A},\\ e_{B}\circ e_{B} & = \text{id}_{B}, \end{aligned} \quad \begin{aligned} f\circ e_{A} & = g,\\ g\circ e_{A} & = f, \end{aligned} \quad \begin{aligned} e_{B}\circ f & = f,\\ e_{B}\circ g & = g. \end{aligned} \]

We may picture $\mathcal{C}$ as follows:

Next, let $\mathcal{D}$ be the walking arrow category $\mathbb {1}$ of Definition 9.2.5.1.1 and let $F\colon \mathcal{C}\to \mathbb {1}$ be the functor given on objects by

\begin{align*} F\webleft (A\webright ) & = 0,\\ F\webleft (B\webright ) & = 1 \end{align*}

and on non-identity morphisms by

\[ \begin{aligned} F\webleft (f\webright ) & = f_{01},\\ F\webleft (g\webright ) & = f_{01}, \end{aligned} \quad \begin{aligned} F\webleft (e_{A}\webright ) & = \text{id}_{0},\\ F\webleft (e_{B}\webright ) & = \text{id}_{1}. \end{aligned} \]

Finally, let $\mathcal{X}=\mathsf{B}\mathbb {Z}_{/2}$ be the walking involution and let $\iota _{A},\iota _{B}\colon \mathsf{B}\mathbb {Z}_{/2}\rightrightarrows \mathcal{C}$ be the inclusion functors from $\mathsf{B}\mathbb {Z}_{/2}$ to $\mathcal{C}$ with

\begin{align*} \iota _{A}\webleft (\bullet \webright ) & = A,\\ \iota _{B}\webleft (\bullet \webright ) & = B. \end{align*}

Since every morphism in $\mathbb {1}$ has a preimage in $\mathcal{C}$ by $F$, the functor $F$ is full. Now, for $F_{*}$ to be full, the map

would need to be surjective. However, as we will show next, we have

\begin{gather*} \text{Nat}\webleft (\iota _{A},\iota _{B}\webright ) = \text{Ø},\\ \text{Nat}\webleft (F\circ \iota _{A},F\circ \iota _{B}\webright ) \cong \text{pt}, \end{gather*}

so this is impossible:

Proof of $\text{Nat}\webleft (\iota _{A},\iota _{B}\webright )=\text{Ø}$: A natural transformation $\alpha \colon \iota _{A}\Rightarrow \iota _{B}$ consists of a morphism

\[ \alpha \colon \underbrace{\iota _{A}\webleft (\bullet \webright )}_{=A}\to \underbrace{\iota _{B}\webleft (\bullet \webright )}_{=B} \]

in $\mathcal{C}$ making the diagram

commute for each $e\in \textup{Hom}_{\mathsf{B}\mathbb {Z}_{/2}}\webleft (\bullet ,\bullet \webright )\cong \mathbb {Z}_{/2}$. We have two cases:
1. If $\alpha =f$, the naturality diagram for the unique nonidentity element of $\mathbb {Z}_{/2}$ is given by
  
  However, $e_{B}\circ f=f$ and $f\circ e_{A}=g$, so this diagram does not commute.
2. If $\alpha =g$, the naturality diagram for the unique nonidentity element of $\mathbb {Z}_{/2}$ is given by
  
  However, $e_{B}\circ g=g$ and $g\circ e_{A}=f$, so this diagram does not commute.
As a result, there are no natural transformations from $\iota _{A}$ to $\iota _{B}$.
Proof of $\text{Nat}\webleft (F\circ \iota _{A},F\circ \iota _{B}\webright )\cong \text{pt}$: A natural transformation

\[ \beta \colon F\circ \iota _{A}\Rightarrow F\circ \iota _{B} \]

consists of a morphism

\[ \beta \colon \underbrace{\webleft [F\circ \iota _{A}\webright ]\webleft (\bullet \webright )}_{=0}\to \underbrace{\webleft [F\circ \iota _{B}\webright ]\webleft (\bullet \webright )}_{=1} \]

in $\mathbb {1}$ making the diagram

commute for each $e\in \textup{Hom}_{\mathsf{B}\mathbb {Z}_{/2}}\webleft (\bullet ,\bullet \webright )\cong \mathbb {Z}_{/2}$. Since the only morphism from $0$ to $1$ in $\mathbb {1}$ is $f_{01}$, we must have $\beta =f_{01}$ if such a transformation were to exist, and in fact it indeed does, as in this case the naturality diagram above becomes

for each $e\in \mathbb {Z}_{/2}$, and this diagram indeed commutes, making $\beta $ into a natural transformation.

This finishes the proof.

Item 3: Interaction With Postcomposition II

Taking $\mathcal{X}=\mathsf{pt}$, it follows by assumption that the functor

\[ F_{*}\colon \mathsf{Fun}\webleft (\mathsf{pt},\mathcal{C}\webright )\to \mathsf{Fun}\webleft (\mathsf{pt},\mathcal{D}\webright ) \]

is full. However, by Item 5 of Proposition 9.10.1.1.2, we have isomorphisms of categories

\begin{align*} \mathsf{Fun}\webleft (\mathsf{pt},\mathcal{C}\webright ) & \cong \mathcal{C},\\ \mathsf{Fun}\webleft (\mathsf{pt},\mathcal{D}\webright ) & \cong \mathcal{D} \end{align*}

and the diagram

commutes. It then follows from Item 1 that $F$ is full.

Item 4: Interaction With Precomposition I

Omitted.

Item 5: Interaction With Precomposition II

See p. 47 of [Baez–Shulman, Lectures on $n$-Categories and Cohomology].

Item 6: Interaction With Precomposition III

Omitted, but see https://unimath.github.io/doc/UniMath/d4de26f//UniMath.CategoryTheory.precomp_fully_faithful.html for a formalised proof.

Item 7: Interaction With Precomposition IV

We claim Item (a), Item (b), Item (c), Item (d), and Item (e) are equivalent:

Item (a) and Item (b) Are Equivalent: This is true by the definition of corepresentably full morphism; see Chapter 11: Graphs, Definition 11.2.2.1.1.
Item (a), Item (c), and Item (d) Are Equivalent: See of .
Item (a) and Item (e) Are Equivalent: See Item (b) of Remark 4.3 of [Adámek–Bashir–Sobral–Velebil, On Functors Which Are Lax Epimorphisms].

This finishes the proof.