regularEpiCategoryOfNormalEpiCategory

English

If C is a normal epi category, then C is a regular epi category.

Русский

Если C — нормальная эпиморфная категория, то C — регулярная эпиморфная категория.

LaTeX

$$$[\text{Category } C] \land [\text{HasZeroMorphisms } C] \land [\text{IsNormalEpiCategory } C] \Rightarrow IsRegularEpiCategory C$$$

Lean4

instance (priority := 100) regularEpiCategoryOfNormalEpiCategory [IsNormalEpiCategory C] : IsRegularEpiCategory C where
  regularEpiOfEpi f
    _ :=
    ⟨by
      haveI := normalEpiOfEpi f
      infer_instance⟩

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