Theorems · Definition · category theory

CategoryTheory.normalEpiOfEpi

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        [CategoryTheory.IsNormalEpiCategory C] → (f : X ⟶ Y) → [CategoryTheory.Epi f] → CategoryTheory.NormalEpi f

In a category in which every epimorphism is normal, we can express every epimorphism as a kernel. This is not an instance because it would create an instance loop.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Cited by

3 results in Mathlib

Foundations

Depth 4 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.IsNormalEpiCategoryCategoryTheory.Epi