Pullback Functor is Functor

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathbf C$ be a metacategory having all pullbacks.

Let $f: C \to D$ be a morphism of $\mathbf C$.

Let $\mathbf C \mathbin / C$ and $\mathbf C \mathbin / D$ be the slice categories over $C$ and $D$, respectively.

Let $f^* : \mathbf C \mathbin / D \to \mathbf C \mathbin / C$ be the pullback functor defined by $f$.


Then $f^*$ is a functor.


Proof

Let $\alpha: A \to D$ be an object of $\mathbf C \mathbin / D$.

Then the identity morphism $\operatorname{id}_\alpha: \alpha \to \alpha$ is by definition $\operatorname{id}_A: A \to A$.


Thus $f^* \operatorname{id}_\alpha$ is by definition the unique morphism fitting:

$\begin{xy}\xymatrix@+1em{ A' \ar[rr]^*{f_\alpha} \ar[dd]_*{f^* \alpha} \ar@{-->}[rd]^*{f^* \mathrm{id}_\alpha} & & A \ar[rd]^*{\mathrm{id}_\alpha} \ar[dd]^(.4)*{\alpha} \\ & A' \ar[ld]^*{f^* \alpha} \ar[rr] |{\hole} ^(.3)*{f_\alpha} & & A \ar[ld]^*{\alpha} \\ C \ar[rr]_*{f} & & D }\end{xy}$

It is apparent that $\operatorname{id}_{A'}$ satisfies this condition.

Since by definition, $\operatorname{id}_{f^* \alpha} = \operatorname{id}_{A'}$, this shows that:

$f^* \operatorname{id}_\alpha = \operatorname{id}_{f^* \alpha}$


Now let $\gamma_1: \alpha_2 \to \alpha_1$ and $\gamma_2: \alpha_3 \to \alpha_2$ be morphisms of $\mathbf C \mathbin / D$.

Then $f^* \left({\gamma_1 \circ \gamma_2}\right)$ is the unique morphism fitting the dashed arrow in:

$\begin{xy}\xymatrix@+1em{ A_3' \ar[rr]^*{f_{\alpha_3}} \ar[dd]_*{f^* \alpha_3} \ar@{-->}[rd] & & A_3 \ar[rd]^*{\gamma_1 \circ \gamma_2} \ar[dd]^(.4)*{\alpha_3} \\ & A_1' \ar[ld]^*{f^* \alpha_1} \ar[rr] |{\hole} ^(.3)*{f_{\alpha_1}} & & A_1 \ar[ld]^*{\alpha_1} \\ C \ar[rr]_*{f} & & D }\end{xy}$

Unfolding the composition $\gamma_1 \circ \gamma_2$ yields the expanded diagram:

$\begin{xy}\xymatrix@+1em{ A_3' \ar[rr]^*{f_{\alpha_3}} \ar[ddd]_*{f^* \alpha_3} \ar[rd]^*{f^* \gamma_2} \ar@{-->}@/_/[rdd] & & A_3 \ar[rd]^*{\gamma_2} \ar[ddd]^*{\alpha_3} \\ & A_2' \ar[d]^*{f^* \gamma_1} \ar[rr] |{\hole} ^(.3)*{f_{\alpha_2}} & & A_2 \ar[d]^*{\gamma_1} \\ & A_1' \ar[ld]^*{f^* \alpha_1} \ar[rr] |{\hole} ^(.3)*{f_{\alpha_1}} & & A_1 \ar[ld]^*{\alpha_1} \\ C \ar[rr]_*{f} & & D }\end{xy}$

in which $f^* \left({\gamma_1 \circ \gamma_2}\right)$ again fits the dashed arrow.

But this means, in particular, that we must have:

$f^* \left({\gamma_1 \circ \gamma_2}\right) = f^* \gamma_1 \circ f^* \gamma_2$


Therefore, $f^*$ is a functor.

$\blacksquare$


Sources