initial_mono_of_strict_initial_objects

English

If a category has strict initial objects, there is a canonical InitialMonoClass structure on C. In particular, for every X the morphism X → I (to the initial object I) satisfies a right-cancellation property coming from the strict initial object.

Русский

Если в категории существуют строгие начальные объекты, существует канонический класс InitialMonoClass на C. В частности, для каждого объекта X морфизм X → I (к начальному объекту I) удовлетворяет свойству правого отменения, вытекающему из строгого начального объекта.

LaTeX

$$$\mathrm{InitialMonoClass}(C)$ с правым отменением, задаваемым строгим начальным свойством$$

Lean4

instance (priority := 100) initial_mono_of_strict_initial_objects : InitialMonoClass C where
  isInitial_mono_from := fun _ hI => { right_cancellation := fun _ _ _ => hI.strict_hom_ext _ _ }

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