# mathlibdocumentation

category_theory.limits.shapes.regular_mono

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

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

We give the constructions

• is_split_mono → regular_mono and
• regular_mono → mono as well as the dual constructions for regular epimorphisms. Additionally, we give the construction
• regular_epi ⟶ strong_epi.

We also define classes regular_mono_category and regular_epi_category for categories in which every monomorphism or epimorphism is regular, and deduce that these categories are strong_mono_categorys resp. strong_epi_categorys.

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

A regular monomorphism is a morphism which is the equalizer of some parallel pair.

Instances of this typeclass
Instances of other typeclasses for category_theory.regular_mono
• category_theory.regular_mono.has_sizeof_inst
theorem category_theory.regular_mono.w_assoc {C : Type u₁} {X Y : C} {f : X Y} [self : category_theory.regular_mono f] {X' : C} (f' : X') :
@[protected, instance]
def category_theory.regular_mono.mono {C : Type u₁} {X Y : C} (f : X Y)  :

Every regular monomorphism is a monomorphism.

@[protected, instance]
noncomputable def category_theory.equalizer_regular {C : Type u₁} {X Y : C} (g h : X Y)  :
Equations
@[protected, instance]
noncomputable def category_theory.regular_mono.of_is_split_mono {C : Type u₁} {X Y : C} (f : X Y)  :

Every split monomorphism is a regular monomorphism.

Equations
def category_theory.regular_mono.lift' {C : Type u₁} {X Y W : C} (f : X Y) (k : W Y)  :
{l // l f = k}

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
def category_theory.regular_of_is_pullback_snd_of_regular {C : Type u₁} {P Q R S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [hr : category_theory.regular_mono h] (comm : f h = g k)  :

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
def category_theory.regular_of_is_pullback_fst_of_regular {C : Type u₁} {P Q R S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [hr : category_theory.regular_mono k] (comm : f h = g k)  :

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
@[protected, instance]
def category_theory.strong_mono_of_regular_mono {C : Type u₁} {X Y : C} (f : X Y)  :
theorem category_theory.is_iso_of_regular_mono_of_epi {C : Type u₁} {X Y : C} (f : X Y) [e : category_theory.epi f] :

A regular monomorphism is an isomorphism if it is an epimorphism.

@[class]
structure category_theory.regular_mono_category (C : Type u₁)  :
Type (max u₁ v₁)
• regular_mono_of_mono : Π {X Y : C} (f : X Y) [_inst_2 : ,

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

Instances of this typeclass
Instances of other typeclasses for category_theory.regular_mono_category
• category_theory.regular_mono_category.has_sizeof_inst
def category_theory.regular_mono_of_mono {C : Type u₁} {X Y : C} (f : X Y)  :

In a category in which every monomorphism is regular, we can express every monomorphism as an equalizer. This is not an instance because it would create an instance loop.

Equations
@[protected, instance]
noncomputable def category_theory.regular_mono_category_of_split_mono_category {C : Type u₁}  :
Equations
@[protected, instance]
@[class]
structure category_theory.regular_epi {C : Type u₁} {X Y : C} (f : X Y) :
Type (max u₁ v₁)
• W : C
• left :
• right :
• w :
• is_colimit :

A regular epimorphism is a morphism which is the coequalizer of some parallel pair.

Instances of this typeclass
Instances of other typeclasses for category_theory.regular_epi
• category_theory.regular_epi.has_sizeof_inst
theorem category_theory.regular_epi.w_assoc {C : Type u₁} {X Y : C} {f : X Y} [self : category_theory.regular_epi f] {X' : C} (f' : Y X') :
@[protected, instance]
def category_theory.regular_epi.epi {C : Type u₁} {X Y : C} (f : X Y)  :

Every regular epimorphism is an epimorphism.

@[protected, instance]
noncomputable def category_theory.coequalizer_regular {C : Type u₁} {X Y : C} (g h : X Y)  :
Equations
@[protected, instance]
noncomputable def category_theory.regular_epi.of_split_epi {C : Type u₁} {X Y : C} (f : X Y)  :

Every split epimorphism is a regular epimorphism.

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

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
def category_theory.regular_of_is_pushout_snd_of_regular {C : Type u₁} {P Q R S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [gr : category_theory.regular_epi g] (comm : f h = g k)  :

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
def category_theory.regular_of_is_pushout_fst_of_regular {C : Type u₁} {P Q R S : C} {f : P Q} {g : P R} {h : Q S} {k : R S} [fr : category_theory.regular_epi f] (comm : f h = g k)  :

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
@[protected, instance]
def category_theory.strong_epi_of_regular_epi {C : Type u₁} {X Y : C} (f : X Y)  :
theorem category_theory.is_iso_of_regular_epi_of_mono {C : Type u₁} {X Y : C} (f : X Y) [m : category_theory.mono f] :

A regular epimorphism is an isomorphism if it is a monomorphism.

@[class]
structure category_theory.regular_epi_category (C : Type u₁)  :
Type (max u₁ v₁)
• regular_epi_of_epi : Π {X Y : C} (f : X Y) [_inst_2 : ,

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

Instances of this typeclass
Instances of other typeclasses for category_theory.regular_epi_category
• category_theory.regular_epi_category.has_sizeof_inst
def category_theory.regular_epi_of_epi {C : Type u₁} {X Y : C} (f : X Y)  :

In a category in which every epimorphism is regular, we can express every epimorphism as a coequalizer. This is not an instance because it would create an instance loop.

Equations
@[protected, instance]
noncomputable def category_theory.regular_epi_category_of_split_epi_category {C : Type u₁}  :
Equations
@[protected, instance]