of_isInitial — Mathlib

English

If an initial object I has the property that every morphism I → X is mono, then C is an InitialMonoClass.

Русский

Если начальный объект I обладает свойством, что каждый морфизм I → X является моно, то C является InitialMonoClass.

LaTeX

$$$(\\exists \\text{I with IsInitial I}) \\wedge (\\forall X, \\text{Mono} (I\\to X)) \\Rightarrow \\text{InitialMonoClass } C$$$

Lean4

/-- To show a category is an `InitialMonoClass` it suffices to give an initial object such that
every morphism out of it is a monomorphism. -/
theorem of_isInitial {I : C} (hI : IsInitial I) (h : ∀ X, Mono (hI.to X)) : InitialMonoClass C where
  isInitial_mono_from {I'} X
    hI' := by
    rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]
    apply mono_comp

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