CatDat

Implication Details

Assumptions: preserves coreflexive equalizers

Assumptions on source category: pushouts

Conclusions: preserves regular monomorphisms

Proof: Let F:CDF : \C \to \D be a functor preserving coreflexive equalizers, where C\C has pushouts; we only need that C\C has cokernel pairs. Let i:XYi : X \to Y be a regular monomorphism in C\C. By Prop. 3.2 at the nLab, ii is the equalizer of the two canonical morphisms u1,u2:YYXYu_1,u_2 : Y \rightrightarrows Y \sqcup_X Y into the cokernel pair of ii. By the universal property of the pushout, there is a morphism :YXYY\nabla : Y \sqcup_X Y \to Y with u1=u2=idY\nabla u_1 = \nabla u_2 = \id_Y. Thus, u1,u2u_1,u_2 is a coreflexive pair. Since FF preserves coreflexive equalizers by assumption, F(i)F(i) is the equalizer of F(u1),F(u2)F(u_1), F(u_2). In particular, F(i)F(i) is a regular monomorphism.

Show 6 functors using this implication