Theorems · Definition · category theory

CategoryTheory.normalMonoOfMono

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

In a category in which every monomorphism is normal, we can express every monomorphism 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.IsNormalMonoCategoryCategoryTheory.Mono