monoCoprodOfHasZeroMorphisms — Mathlib

English

In any category with zero morphisms, the left injection into a binary coproduct A ⊔ B is mono; i.e., coprod.inl: A → A ⊔ B is a monomorphism.

Русский

В любой категории с нулевыми морфизмами левый включающий из A в двойной coproduct A ⊔ B является мономорфизмом; то есть coprod.inl: A → A ⊔ B моно.

LaTeX

$$$\\forall A,B,\\ Mono\\ (\\mathrm{coprod.inl}: A \\to A \\amalg B).$$$

Lean4

instance (priority := 100) monoCoprodOfHasZeroMorphisms [HasZeroMorphisms C] : MonoCoprod C :=
  ⟨fun A B c hc =>
    by
    haveI : IsSplitMono c.inl := IsSplitMono.mk' (SplitMono.mk (hc.desc (BinaryCofan.mk (𝟙 A) 0)) (IsColimit.fac _ _ _))
    infer_instance⟩

Похожие утверждения