initialMonoClass_of_coproductsDisjoint

English

If the category has BinaryCoproductsDisjoint, then there is an InitialMonoClass C.

Русский

Если у категорий есть BinaryCoproductDisjoint, то существует InitialMonoClass C.

LaTeX

$$$\\text{InitialMonoClass}\\ C$$$

Lean4

/-- If `C` has disjoint coproducts, any morphism out of initial is mono. Note it isn't true in
general that `C` has strict initial objects, for instance consider the category of types and
partial functions. -/
theorem initialMonoClass_of_coproductsDisjoint [BinaryCoproductsDisjoint C] : InitialMonoClass C where
  isInitial_mono_from X
    hI :=
    .of_binaryCoproductDisjoint_left (CategoryTheory.CategoryStruct.id X)
      { desc := fun s : BinaryCofan _ _ => s.inr
        fac := fun _s j => Discrete.casesOn j fun j => WalkingPair.casesOn j (hI.hom_ext _ _) (id_comp _)
        uniq := fun (_s : BinaryCofan _ _) _m w => (id_comp _).symm.trans (w ⟨WalkingPair.right⟩) }

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