# Documentation

Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

# 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₁} [] {X : C} {Y : C} (f : X Y) :
Type (max u₁ v₁)

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

Instances
def CategoryTheory.equivalenceReflectsNormalMono {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} {f : X Y} (hf : CategoryTheory.NormalMono (F.map f)) :

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

Instances For
instance CategoryTheory.NormalMono.regularMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [I : ] :

Every normal monomorphism is a regular monomorphism.

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

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.

Instances For
def CategoryTheory.normalOfIsPullbackSndOfNormal {C : Type u₁} [] {P : C} {Q : C} {R : C} {S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [hn : ] (comm : ) (t : ) :

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.

Instances For
def CategoryTheory.normalOfIsPullbackFstOfNormal {C : Type u₁} [] {P : C} {Q : C} {R : C} {S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} (comm : ) (t : ) :

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.

Instances For
class CategoryTheory.NormalMonoCategory (C : Type u₁) [] :
Type (max u₁ v₁)
• normalMonoOfMono : {X Y : C} → (f : X Y) → [inst : ] →

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

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

Instances
def CategoryTheory.normalMonoOfMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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.

Instances For
class CategoryTheory.NormalEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Type (max u₁ v₁)

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

Instances
def CategoryTheory.equivalenceReflectsNormalEpi {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} {f : X Y} (hf : CategoryTheory.NormalEpi (F.map f)) :

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

Instances For
instance CategoryTheory.NormalEpi.regularEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [I : ] :

Every normal epimorphism is a regular epimorphism.

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

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

Instances For
def CategoryTheory.normalOfIsPushoutSndOfNormal {C : Type u₁} [] {P : C} {Q : C} {R : C} {S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [gn : ] (comm : ) :

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.

Instances For
def CategoryTheory.normalOfIsPushoutFstOfNormal {C : Type u₁} [] {P : C} {Q : C} {R : C} {S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} (comm : ) :

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.

Instances For
def CategoryTheory.normalEpiOfNormalMonoUnop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (m : ) :

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

Instances For
def CategoryTheory.normalMonoOfNormalEpiUnop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (m : CategoryTheory.NormalEpi f.unop) :

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

Instances For
class CategoryTheory.NormalEpiCategory (C : Type u₁) [] :
Type (max u₁ v₁)
• normalEpiOfEpi : {X Y : C} → (f : X Y) → [inst : ] →

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

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

Instances
def CategoryTheory.normalEpiOfEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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.

Instances For