English
Let C be a category with a zero object and zero morphisms, and X,Y objects that have a binary coproduct X ⊔ Y. Then the pushout of the two zero morphisms 0:0→X and 0:0→Y along the canonical injections into the coproduct X ⊔ Y exists and is given by the coproduct injections coprod.inl and coprod.inr.
Русский
Пусть C — категория с нулевым объектом и нулевыми морфизмами, и пусть X, Y — объекты, существующий двоичный копродукт X ⊔ Y. Тогда пушаут двух нулевых морфизмов 0:0→X и 0:0→Y существует и задан инъекциями coproduct: coprod.inl, coprod.inr.
LaTeX
$$$IsPushout(0:0\to X,\ 0:0\to Y,\ coprod.inl,\ coprod.inr)$$$
Lean4
theorem of_hasBinaryCoproduct [HasBinaryCoproduct X Y] [HasZeroObject C] [HasZeroMorphisms C] :
IsPushout (0 : 0 ⟶ X) (0 : 0 ⟶ Y) coprod.inl coprod.inr := by
convert @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial <;> subsingleton
