English
In an Abelian category, pushouts exist. For any pair f: X → Y and g: X → Z there is a pushout object Pushout(f,g) together with morphisms i_Y: Y → Pushout and i_Z: Z → Pushout such that i_Y ∘ f = i_Z ∘ g and the pushout satisfies the universal property with respect to morphisms from Y and Z to any W.
Русский
В абелевой категории существуют совпадения. Для любых стрелок f: X → Y и g: X → Z существует объект Pushout(f,g) с морфизмами i_Y: Y → Pushout и i_Z: Z → Pushout, такие что i_Y ∘ f = i_Z ∘ g, и этот пушаут удовлетворяет универсальному свойству с любыми стрелками из Y и Z в произвольный W.
LaTeX
$$$\\\\forall X,Y,Z \\\\in \\\\mathrm{Obj}(C), \\\\forall f: X \\\\to Y, \\\\forall g: X \\\\to Z, \\\\exists P, i_Y: Y \\\\to P, i_Z: Z \\\\to P, i_Y \\\\circ f = i_Z \\\\circ g \\\\land \\\\forall W, h_Y: Y \\\\to W, h_Z: Z \\\\to W, h_Y \\\\circ f = h_Z \\\\circ g \\\\Rightarrow \\\\exists! u: P \\\\to W, h_Y = u \\\\\\circ i_Y, h_Z = u \\\\\\circ i_Z.$$
Lean4
/-- Any abelian category has pushouts -/
instance (priority := 100) hasPushouts : HasPushouts C :=
hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers C
