# Documentation

Mathlib.CategoryTheory.Limits.Shapes.RegularMono

# 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.

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

Every regular monomorphism is a monomorphism.

instance CategoryTheory.equalizerRegular {C : Type u₁} [] {X : C} {Y : C} (g : X Y) (h : X Y) :
instance CategoryTheory.RegularMono.ofIsSplitMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every split monomorphism is a regular monomorphism.

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 // }

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.

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.

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.

Instances For
instance CategoryTheory.strongMono_of_regularMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
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₁)
• regularMonoOfMono : {X Y : C} → (f : X Y) → [inst : ] →

Every monomorphism is a regular monomorphism

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

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.

Instances For
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.

Instances
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 CategoryTheory.RegularEpi.epi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every regular epimorphism is an epimorphism.

instance CategoryTheory.coequalizerRegular {C : Type u₁} [] {X : C} {Y : C} (g : X Y) (h : X Y) :
instance CategoryTheory.RegularEpi.ofSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every split epimorphism is a regular epimorphism.

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 // }

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.

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.

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.

Instances For
instance CategoryTheory.strongEpi_of_regularEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
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₁)
• regularEpiOfEpi : {X Y : C} → (f : X Y) → [inst : ] →

Everyone epimorphism is a regular epimorphism

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

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.

Instances For