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 NormalMonoCategory and NormalEpiCategory for classes in which every monomorphism or epimorphism is normal, and deduce that these categories are RegularMonoCategorys resp. RegularEpiCategorys.

class CategoryTheory.NormalMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.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 ⟶ CategoryTheory.NormalMono.Z f

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

• w : CategoryTheory.CategoryStruct.comp f CategoryTheory.NormalMono.g = 0

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

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

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

theorem CategoryTheory.NormalMono.w {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {f : X ⟶ Y} [self : CategoryTheory.NormalMono f], CategoryTheory.CategoryStruct.comp f CategoryTheory.NormalMono.g = 0

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

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

Every normal monomorphism is a regular monomorphism.

Equations

• CategoryTheory.NormalMono.regularMono f = { Z := CategoryTheory.NormalMono.Z f, left := CategoryTheory.NormalMono.g, right := 0, w := ⋯, isLimit := CategoryTheory.NormalMono.isLimit }

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

Equations

• CategoryTheory.NormalMono.lift' f k h = CategoryTheory.Limits.KernelFork.IsLimit.lift' CategoryTheory.NormalMono.isLimit k h

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.normalOfIsPullbackFstOfNormal comm t = CategoryTheory.normalOfIsPullbackSndOfNormal ⋯ (CategoryTheory.Limits.PullbackCone.flipIsLimit t)

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

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

• normalMonoOfMono : {X Y : C} → (f : X ⟶ Y) → [inst : CategoryTheory.Mono f] → CategoryTheory.NormalMono f

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

def CategoryTheory.normalMonoOfMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.NormalMonoCategory 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.

Equations

• CategoryTheory.normalMonoOfMono f = CategoryTheory.NormalMonoCategory.normalMonoOfMono f

@[instance 100]

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

Equations

• CategoryTheory.regularMonoCategoryOfNormalMonoCategory = { regularMonoOfMono := fun {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.Mono f) => inferInstance }

class CategoryTheory.NormalEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.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 : CategoryTheory.NormalEpi.W f ⟶ X

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

• w : CategoryTheory.CategoryStruct.comp CategoryTheory.NormalEpi.g f = 0

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

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

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

theorem CategoryTheory.NormalEpi.w {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {f : X ⟶ Y} [self : CategoryTheory.NormalEpi f], CategoryTheory.CategoryStruct.comp CategoryTheory.NormalEpi.g f = 0

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

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

Every normal epimorphism is a regular epimorphism.

Equations

• CategoryTheory.NormalEpi.regularEpi f = { W := CategoryTheory.NormalEpi.W f, left := CategoryTheory.NormalEpi.g, right := 0, w := ⋯, isColimit := CategoryTheory.NormalEpi.isColimit }

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

Equations

• CategoryTheory.NormalEpi.desc' f k h = CategoryTheory.Limits.CokernelCofork.IsColimit.desc' CategoryTheory.NormalEpi.isColimit k h

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.normalOfIsPushoutFstOfNormal comm t = CategoryTheory.normalOfIsPushoutSndOfNormal ⋯ (CategoryTheory.Limits.PushoutCocone.flipIsColimit t)

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

• normalEpiOfEpi : {X Y : C} → (f : X ⟶ Y) → [inst : CategoryTheory.Epi f] → CategoryTheory.NormalEpi f

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

def CategoryTheory.normalEpiOfEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.NormalEpiCategory 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.

Equations

• CategoryTheory.normalEpiOfEpi f = CategoryTheory.NormalEpiCategory.normalEpiOfEpi f

@[instance 100]

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

Equations

• CategoryTheory.regularEpiCategoryOfNormalEpiCategory = { regularEpiOfEpi := fun {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.Epi f) => inferInstance }