English
A commutative square in a preadditive category is a pushout square iff the induced diagram with the cokernel is a cokernel diagram; equivalently, there is an equivalence between the property of being a pushout and the property that the cokernel cofork is colim.
Русский
Любой коммутативный квадрат в предварительно аддитивной категории является pushout-квадратом тогда и только тогда, когда соответствующая диаграмма с коконелем образует кокон (кококое копи). Эквивалентность между свойством being pushout и тем, что cokernel cofork является колим.
LaTeX
$$$\\text{IsPushout}(sq) \\simeq \\text{IsColimit}(sq\\,\\text{cokernelCofork})$$$
Lean4
/-- A commutative square in a preadditive category is a pushout square iff
the corresponding diagram `X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0` makes `X₄` a cokernel. -/
noncomputable def isPushoutEquivIsColimitCokernelCofork : sq.IsPushout ≃ IsColimit sq.cokernelCofork :=
Equiv.trans
{ toFun := fun h ↦ h.isColimit
invFun := fun h ↦ IsPushout.mk _ h
right_inv := fun _ ↦ Subsingleton.elim _ _ } sq.commSq.isColimitEquivIsColimitCokernelCofork
