mathlib documentation

category_theory.limits.shapes.regular_mono

Definitions and basic properties of regular and normal monomorphisms and epimorphisms.

A regular monomorphism is a morphism that is the equalizer of some parallel pair. A normal monomorphism is a morphism that is the kernel of some other morphism.

We give the constructions

@[instance]

Every regular monomorphism is a monomorphism.

@[instance]

Every split monomorphism is a regular monomorphism.

Equations

If f is a regular mono, then any map k : W ⟶ Y equalizing regular_mono.left and regular_mono.right induces a morphism l : W ⟶ X such that l ≫ f = k.

Equations

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

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

Equations

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

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

Equations
@[class]
structure category_theory.normal_mono {C : Type u₁} [category_theory.category C] {X Y : C} [category_theory.limits.has_zero_morphisms C] :
(X Y)Type (max u₁ v₁)

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

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

Equations

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

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

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
@[instance]

Every regular epimorphism is an epimorphism.

@[instance]

Every split epimorphism is a regular epimorphism.

Equations

If f is a regular epi, then every morphism k : X ⟶ W coequalizing regular_epi.left and regular_epi.right induces l : Y ⟶ W such that f ≫ l = k.

Equations

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

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

Equations

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

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

Equations
@[class]
structure category_theory.normal_epi {C : Type u₁} [category_theory.category C] {X Y : C} [category_theory.limits.has_zero_morphisms C] :
(X Y)Type (max u₁ v₁)

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

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

Equations

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

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

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