CatDat

Implication Details

Claim: Given a functor whose codomain has biproducts, and whose domain has biproducts, if it preserves preserves finite coproducts, then it preserves preserves finite products.

Proof: Let C,D\C,\D be categories with biproducts, and let F:CDF : \C \to \D be a functor preserving finite coproducts. In particular, FF preserves the zero object. Since zero morphisms are precisely the morphisms that factor through the zero object, FF preserves zero morphisms.

Let A,BCA,B \in \C be objects with coproduct injections iA:AABi_A : A \to A \sqcup B and iB:BABi_B : B \to A \sqcup B. Since C\C has biproducts, there are projections pA:ABAp_A : A \sqcup B \to A and pB:ABBp_B : A \sqcup B \to B satisfying: pAiA=idApBiA=0pAiB=0pBiB=idBiApA+iBpB=idAB.\begin{align*} p_A i_A &= \id_A\\ p_B i_A &= 0\\ p_A i_B &= 0\\ p_B i_B &= \id_B\\ i_A p_A + i_B p_B &= \id_{A \sqcup B}. \end{align*} By assumption, F(AB)F(A \sqcup B) is a coproduct of F(A)F(A) and F(B)F(B) with coproduct injections F(iA)F(i_A) and F(iB)F(i_B). Since D\D has biproducts, there are product projections qA:F(AB)F(A)q_A : F(A \sqcup B) \to F(A) and qB:F(AB)F(B)q_B : F(A \sqcup B) \to F(B) satisfying: qAF(iA)=idF(A)qBF(iA)=0qAF(iB)=0qBF(iB)=idF(B)F(iA)qA+F(iB)qB=idF(AB).\begin{align*} q_A F(i_A) &= \id_{F(A)}\\ q_B F(i_A) &= 0\\ q_A F(i_B) &= 0\\ q_B F(i_B) &= \id_{F(B)}\\ F(i_A) q_A + F(i_B) q_B &= \id_{F(A \sqcup B)}. \end{align*} We need to show that F(pA)=qAF(p_A) = q_A; the proof that F(pB)=qBF(p_B) = q_B is similar. Both sides are morphisms F(AB)F(A)F(A \sqcup B) \to F(A), and since F(AB)F(A \sqcup B) is a coproduct of F(A)F(A) and F(B)F(B), it suffices to verify the equality after precomposing with the two coproduct injections F(iA)F(i_A) and F(iB)F(i_B). We compute qAF(iA)=idF(A)=F(idA)=F(pAiA)=F(pA)F(iA)q_A F(i_A) = \id_{F(A)} = F(\id_A) = F(p_A i_A) = F(p_A) F(i_A) and qAF(iB)=0=F(0)=F(pAiB)=F(pA)F(iB).q_A F(i_B) = 0 = F(0) = F(p_A i_B) = F(p_A) F(i_B).
Remark: It now follows that FF is also additive, i.e., for two morphisms f,g:ABf,g : A \rightrightarrows B, we have F(f+g)=F(f)+F(g)F(f+g) = F(f) + F(g). In fact, f+gf+g decomposes as A(f,g)B×Bμ1BBB,A \xrightarrow{(f,g)} B \times B \xrightarrow{\mu^{-1}} B \sqcup B \xrightarrow{\nabla} B, and each of these components is preserved by FF.