CatDat

Implication Details

Claim: Given a morphism whose category has zero morphisms, if it is constant, then it is a zero morphism.

Proof: Let $f : A \to B$ be a constant morphism in a category with zero morphisms. Then it is the zero morphism $0_{A,B}$ because $$f = f \circ \id_A = f \circ 0_{A,A} = 0_{A,B}.$$ Furthermore, $0_{A,B}$ is coconstant because for all $g,h : B \rightrightarrows C$ we have $$g \circ 0_{A,B} = 0_{A,C} = h \circ 0_{A,B}.$$ (A similar argument shows that $0_{A,B}$ is also constant.)