Definitions and basic properties of normal monomorphisms and epimorphisms.

A normal monomorphism is a morphism that is the kernel of some other morphism.

We give the construction NormalMono → RegularMono (CategoryTheory.NormalMono.regularMono) as well as the dual construction for normal epimorphisms. We show equivalences reflect normal monomorphisms (CategoryTheory.equivalenceReflectsNormalMono), and that the pullback of a normal monomorphism is normal (CategoryTheory.normalOfIsPullbackSndOfNormal).

We also define classes IsNormalMonoCategory and IsNormalEpiCategory for categories in which every monomorphism or epimorphism is normal, and deduce that these categories are RegularMonoCategorys resp. RegularEpiCategorys.

class CategoryTheory.NormalMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] (f : X ⟶ Y) : Type (max u₁ v₁)

A normal monomorphism is a morphism which is the kernel of some morphism.

• Z : C

  A normal monomorphism is a morphism which is the kernel of some morphism.

• g : Y ⟶ Z f

  A normal monomorphism is a morphism which is the kernel of some morphism.

• w : CategoryStruct.comp f g = 0

  A normal monomorphism is a morphism which is the kernel of some morphism.

• isLimit : Limits.IsLimit (Limits.KernelFork.ofι f ⋯)

  A normal monomorphism is a morphism which is the kernel of some morphism.

@[implicit_reducible]

noncomputable def CategoryTheory.equivalenceReflectsNormalMono {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₁, u₂} D] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.IsEquivalence] {X Y : C} {f : X ⟶ Y} (hf : NormalMono (F.map f)) : NormalMono f

If F is an equivalence and F.map f is a normal mono, then f is a normal mono.

def CategoryTheory.NormalMono.regularMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] (f : X ⟶ Y) [I : NormalMono f] : RegularMono f

Every normal monomorphism is a regular monomorphism.

@[instance 100]

instance CategoryTheory.instIsRegularMonoOfNormalMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] (f : X ⟶ Y) [I : NormalMono f] : IsRegularMono f

def CategoryTheory.NormalMono.lift' {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] {W : C} (f : X ⟶ Y) [hf : NormalMono f] (k : W ⟶ Y) (h : CategoryStruct.comp k g = 0) : { l : W ⟶ X // CategoryStruct.comp l f = k }

If f is a normal mono, then any map k : W ⟶ Y such that k ≫ normal_mono.g = 0 induces a morphism l : W ⟶ X such that l ≫ f = k.

@[implicit_reducible]

def CategoryTheory.normalOfIsPullbackSndOfNormal {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [hn : NormalMono h] (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) (t : Limits.IsLimit (Limits.PullbackCone.mk f g comm)) : NormalMono g

The second leg of a pullback cone is a normal monomorphism if the right component is too.

See also pullback.sndOfMono for the basic monomorphism version, and normalOfIsPullbackFstOfNormal for the flipped version.

@[implicit_reducible]

def CategoryTheory.normalOfIsPullbackFstOfNormal {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [NormalMono k] (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) (t : Limits.IsLimit (Limits.PullbackCone.mk f g comm)) : NormalMono f

The first leg of a pullback cone is a normal monomorphism if the left component is too.

See also pullback.fstOfMono for the basic monomorphism version, and normalOfIsPullbackSndOfNormal for the flipped version.

@[implicit_reducible]

def CategoryTheory.NormalMono.ofArrowIso {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (hf : NormalMono f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : NormalMono f'

Transport a NormalMono structure via an isomorphism of arrows.

class CategoryTheory.IsNormalMonoCategory (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] : Prop

A normal mono category is a category in which every monomorphism is normal.

• normalMonoOfMono {X Y : C} (f : X ⟶ Y) [Mono f] : Nonempty (NormalMono f)

  A normal mono category is a category in which every monomorphism is normal.

@[implicit_reducible]

noncomputable def CategoryTheory.normalMonoOfMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] [IsNormalMonoCategory C] (f : X ⟶ Y) [Mono f] : 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.

@[instance 100]

instance CategoryTheory.regularMonoCategoryOfNormalMonoCategory {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [IsNormalMonoCategory C] : IsRegularMonoCategory C

class CategoryTheory.NormalEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] (f : X ⟶ Y) : Type (max u₁ v₁)

A normal epimorphism is a morphism which is the cokernel of some morphism.

• W : C

  A normal epimorphism is a morphism which is the cokernel of some morphism.

• g : W f ⟶ X

  A normal epimorphism is a morphism which is the cokernel of some morphism.

• w : CategoryStruct.comp g f = 0

  A normal epimorphism is a morphism which is the cokernel of some morphism.

• isColimit : Limits.IsColimit (Limits.CokernelCofork.ofπ f ⋯)

  A normal epimorphism is a morphism which is the cokernel of some morphism.

@[implicit_reducible]

noncomputable def CategoryTheory.equivalenceReflectsNormalEpi {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₁, u₂} D] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.IsEquivalence] {X Y : C} {f : X ⟶ Y} (hf : NormalEpi (F.map f)) : NormalEpi f

If F is an equivalence and F.map f is a normal epi, then f is a normal epi.

def CategoryTheory.NormalEpi.regularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] (f : X ⟶ Y) [I : NormalEpi f] : RegularEpi f

Every normal epimorphism is a regular epimorphism.

@[instance 100]

instance CategoryTheory.instIsRegularEpiOfNormalEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] (f : X ⟶ Y) [I : NormalEpi f] : IsRegularEpi f

def CategoryTheory.NormalEpi.desc' {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] {W : C} (f : X ⟶ Y) [nef : NormalEpi f] (k : X ⟶ W) (h : CategoryStruct.comp g k = 0) : { l : Y ⟶ W // CategoryStruct.comp f l = k }

If f is a normal epi, then every morphism k : X ⟶ W satisfying NormalEpi.g ≫ k = 0 induces l : Y ⟶ W such that f ≫ l = k.

@[implicit_reducible]

def CategoryTheory.normalOfIsPushoutSndOfNormal {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [gn : NormalEpi g] (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) (t : Limits.IsColimit (Limits.PushoutCocone.mk h k comm)) : NormalEpi h

The second leg of a pushout cocone is a normal epimorphism if the right component is too.

See also pushout.sndOfEpi for the basic epimorphism version, and normalOfIsPushoutFstOfNormal for the flipped version.

@[implicit_reducible]

def CategoryTheory.normalOfIsPushoutFstOfNormal {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [NormalEpi f] (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) (t : Limits.IsColimit (Limits.PushoutCocone.mk h k comm)) : NormalEpi k

The first leg of a pushout cocone is a normal epimorphism if the left component is too.

See also pushout.fstOfEpi for the basic epimorphism version, and normalOfIsPushoutSndOfNormal for the flipped version.

@[implicit_reducible]

def CategoryTheory.NormalEpi.ofArrowIso {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (hf : NormalEpi f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : NormalEpi f'

Transport a NormalEpi structure via an isomorphism of arrows.

@[implicit_reducible]

def CategoryTheory.normalEpiOfNormalMonoUnop {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : NormalMono f.unop) : NormalEpi f

A normal mono becomes a normal epi in the opposite category.

@[implicit_reducible]

def CategoryTheory.normalMonoOfNormalEpiUnop {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : NormalEpi f.unop) : NormalMono f

A normal epi becomes a normal mono in the opposite category.

class CategoryTheory.IsNormalEpiCategory (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] : Prop

A normal epi category is a category in which every epimorphism is normal.

• normalEpiOfEpi {X Y : C} (f : X ⟶ Y) [Epi f] : Nonempty (NormalEpi f)

  A normal epi category is a category in which every epimorphism is normal.

@[implicit_reducible]

noncomputable def CategoryTheory.normalEpiOfEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroMorphisms C] [IsNormalEpiCategory C] (f : X ⟶ Y) [Epi f] : 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.

@[instance 100]

instance CategoryTheory.regularEpiCategoryOfNormalEpiCategory {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [IsNormalEpiCategory C] : IsRegularEpiCategory C