English
Let C be a category with zero morphisms. If X and Y have a binary coproduct X ⨿ Y, then the right coprojection coprod.inr: Y → X ⨿ Y is a split monomorphism; equivalently there exists a morphism s: X ⨿ Y → Y with coprod.inr ≫ s = id_Y (take s = coprod.desc 0 (id_Y)).
Русский
Пусть C — категория с нулевыми морфизмами. Если существуют копродукт X ⨿ Y, то копроинъекция справа coprod.inr: Y → X ⨿ Y является разделимым мономорфизмом; существует s: X ⨿ Y → Y с coprod.inr ≫ s = id_Y (например s = coprod.desc 0 (id_Y)).
LaTeX
$$$\exists s: X \oplus Y \to Y\quad\text{such that}\quad coprod.inr \;\circ\; s = \mathrm{id}_Y.$$$
Lean4
/-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms. -/
instance isSplitMono_coprod_inr [HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] :
IsSplitMono (coprod.inr : Y ⟶ X ⨿ Y) :=
IsSplitMono.mk' { retraction := coprod.desc 0 (𝟙 Y) }
