# mathlibdocumentation

category_theory.limits.shapes.normal_mono

# 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 normal_mono → regular_mono (category_theory.normal_mono.regular_mono) as well as the dual construction for normal epimorphisms. We show equivalences reflect normal monomorphisms (category_theory.equivalence_reflects_normal_mono), and that the pullback of a normal monomorphism is normal (category_theory.normal_of_is_pullback_snd_of_normal).

@[class]
structure category_theory.normal_mono {C : Type u₁} {X Y : C} (f : X Y) :
Type (max u₁ v₁)
• Z : C
• g :
• w :
• is_limit :

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

def category_theory.equivalence_reflects_normal_mono {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} {f : X Y} (hf : category_theory.normal_mono (F.map f)) :

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

Equations
@[instance]
def category_theory.normal_mono.regular_mono {C : Type u₁} {X Y : C} (f : X Y)  :

Every normal monomorphism is a regular monomorphism.

Equations
def category_theory.normal_mono.lift' {C : Type u₁} {X Y : C} {W : C} (f : X Y) (k : W Y) (h : = 0) :
{l // 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
def category_theory.normal_of_is_pullback_snd_of_normal {C : Type u₁} {P Q R S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [hn : category_theory.normal_mono h] (comm : f h = g k)  :

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

See also pullback.snd_of_mono for the basic monomorphism version, and normal_of_is_pullback_fst_of_normal for the flipped version.

Equations
def category_theory.normal_of_is_pullback_fst_of_normal {C : Type u₁} {P Q R S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [hn : category_theory.normal_mono k] (comm : f h = g k)  :

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

See also pullback.fst_of_mono for the basic monomorphism version, and normal_of_is_pullback_snd_of_normal for the flipped version.

Equations
@[class]
structure category_theory.normal_epi {C : Type u₁} {X Y : C} (f : X Y) :
Type (max u₁ v₁)
• W : C
• g :
• w :
• is_colimit :

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

def category_theory.equivalence_reflects_normal_epi {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} {f : X Y} (hf : category_theory.normal_epi (F.map f)) :

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

Equations
@[instance]
def category_theory.normal_epi.regular_epi {C : Type u₁} {X Y : C} (f : X Y)  :

Every normal epimorphism is a regular epimorphism.

Equations
def category_theory.normal_epi.desc' {C : Type u₁} {X Y : C} {W : C} (f : X Y) (k : X W) (h : = 0) :
{l // f l = k}

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.

Equations
def category_theory.normal_of_is_pushout_snd_of_normal {C : Type u₁} {P Q R S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [gn : category_theory.normal_epi g] (comm : f h = g k)  :

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

See also pushout.snd_of_epi for the basic epimorphism version, and normal_of_is_pushout_fst_of_normal for the flipped version.

Equations
def category_theory.normal_of_is_pushout_fst_of_normal {C : Type u₁} {P Q R S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [hn : category_theory.normal_epi f] (comm : f h = g k)  :

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

See also pushout.fst_of_epi for the basic epimorphism version, and normal_of_is_pushout_snd_of_normal for the flipped version.

Equations
def category_theory.normal_epi_of_normal_mono_unop {C : Type u₁} {X Y : Cᵒᵖ} (f : X Y)  :

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

Equations
def category_theory.normal_mono_of_normal_epi_unop {C : Type u₁} {X Y : Cᵒᵖ} (f : X Y)  :

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

Equations