# 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

• IsSplitMono → RegularMono and
• RegularMono → Mono as well as the dual constructions for regular epimorphisms. Additionally, we give the construction
• RegularEpi ⟶ StrongEpi.

We also define classes RegularMonoCategory and RegularEpiCategory for categories in which every monomorphism or epimorphism is regular, and deduce that these categories are StrongMonoCategorys resp. StrongEpiCategorys.

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

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

• Z : C

An object in C

• left :

A map from the codomain of f to Z

• right :

Another map from the codomain of f to Z

• w : CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.left = CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.right

f equalizes the two maps

• isLimit :

f is the equalizer of the two maps

Instances
theorem CategoryTheory.RegularMono.w {C : Type u₁} [] {X : C} {Y : C} {f : X Y} [self : ] :
CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.left = CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.right

f equalizes the two maps

theorem CategoryTheory.RegularMono.w_assoc {C : Type u₁} [] {X : C} {Y : C} {f : X Y} [self : ] {Z : C} (h : ) :
@[instance 100]
instance CategoryTheory.RegularMono.mono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every regular monomorphism is a monomorphism.

Equations
• =
instance CategoryTheory.equalizerRegular {C : Type u₁} [] {X : C} {Y : C} (g : X Y) (h : X Y) :
Equations
• One or more equations did not get rendered due to their size.
@[instance 100]
instance CategoryTheory.RegularMono.ofIsSplitMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every split monomorphism is a regular monomorphism.

Equations
• One or more equations did not get rendered due to their size.
def CategoryTheory.RegularMono.lift' {C : Type u₁} [] {X : C} {Y : C} {W : C} (f : X Y) (k : W Y) (h : CategoryTheory.CategoryStruct.comp k CategoryTheory.RegularMono.left = CategoryTheory.CategoryStruct.comp k CategoryTheory.RegularMono.right) :
{ l : W X // }

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

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

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

See also Pullback.sndOfMono for the basic monomorphism version, and regularOfIsPullbackFstOfRegular for the flipped version.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.regularOfIsPullbackFstOfRegular {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 regular monomorphism if the left component is too.

See also Pullback.fstOfMono for the basic monomorphism version, and regularOfIsPullbackSndOfRegular for the flipped version.

Equations
Instances For
@[instance 100]
instance CategoryTheory.strongMono_of_regularMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Equations
• =
theorem CategoryTheory.isIso_of_regularMono_of_epi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

class CategoryTheory.RegularMonoCategory (C : Type u₁) [] :
Type (max u₁ v₁)

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

• regularMonoOfMono : {X Y : C} → (f : X Y) → [inst : ] →

Every monomorphism is a regular monomorphism

Instances
def CategoryTheory.regularMonoOfMono {C : Type u₁} [] {X : C} {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
Instances For
@[instance 100]
Equations
• CategoryTheory.regularMonoCategoryOfSplitMonoCategory = { regularMonoOfMono := fun {X Y : C} (f : X Y) (x : ) => inferInstance }
@[instance 100]
Equations
• =
class CategoryTheory.RegularEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Type (max u₁ v₁)

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

• W : C

An object from C

• left :

Two maps to the domain of f

• right :

Two maps to the domain of f

• w : CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left f = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right f

f coequalizes the two maps

• isColimit :

f is the coequalizer

Instances
theorem CategoryTheory.RegularEpi.w {C : Type u₁} [] {X : C} {Y : C} {f : X Y} [self : ] :
CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left f = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right f

f coequalizes the two maps

theorem CategoryTheory.RegularEpi.w_assoc {C : Type u₁} [] {X : C} {Y : C} {f : X Y} [self : ] {Z : C} (h : Y Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right
@[instance 100]
instance CategoryTheory.RegularEpi.epi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every regular epimorphism is an epimorphism.

Equations
• =
instance CategoryTheory.coequalizerRegular {C : Type u₁} [] {X : C} {Y : C} (g : X Y) (h : X Y) :
Equations
• One or more equations did not get rendered due to their size.
noncomputable def CategoryTheory.regularEpiOfKernelPair {C : Type u₁} [] {B : C} {X : C} (f : X B) :

A morphism which is a coequalizer for its kernel pair is a regular epi.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[instance 100]
instance CategoryTheory.RegularEpi.ofSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every split epimorphism is a regular epimorphism.

Equations
• One or more equations did not get rendered due to their size.
def CategoryTheory.RegularEpi.desc' {C : Type u₁} [] {X : C} {Y : C} {W : C} (f : X Y) (k : X W) (h : CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left k = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right k) :
{ l : Y W // }

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

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

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

See also Pushout.sndOfEpi for the basic epimorphism version, and regularOfIsPushoutFstOfRegular for the flipped version.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.regularOfIsPushoutFstOfRegular {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 regular epimorphism if the left component is too.

See also Pushout.fstOfEpi for the basic epimorphism version, and regularOfIsPushoutSndOfRegular for the flipped version.

Equations
Instances For
@[instance 100]
instance CategoryTheory.strongEpi_of_regularEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Equations
• =
theorem CategoryTheory.isIso_of_regularEpi_of_mono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

class CategoryTheory.RegularEpiCategory (C : Type u₁) [] :
Type (max u₁ v₁)

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

• regularEpiOfEpi : {X Y : C} → (f : X Y) → [inst : ] →

Everyone epimorphism is a regular epimorphism

Instances
def CategoryTheory.regularEpiOfEpi {C : Type u₁} [] {X : C} {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
Instances For
@[instance 100]
Equations
• CategoryTheory.regularEpiCategoryOfSplitEpiCategory = { regularEpiOfEpi := fun {X Y : C} (f : X Y) (x : ) => inferInstance }
@[instance 100]
Equations
• =