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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) : Type (max u₁ v₁)

• Z : C

  An object in C

• left : Y ⟶ CategoryTheory.RegularMono.Z f

  A map from the codomain of f to Z

• right : Y ⟶ CategoryTheory.RegularMono.Z f

  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 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f (_ : CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.left = CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.right))

  f is the equalizer of the two maps

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

theorem CategoryTheory.RegularMono.w_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {f : X ⟶ Y} [self : CategoryTheory.RegularMono f] {Z : C} (h : CategoryTheory.RegularMono.Z f ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.RegularMono.left h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.RegularMono.right h)

instance CategoryTheory.RegularMono.mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.RegularMono f] : CategoryTheory.Mono f

Every regular monomorphism is a monomorphism.

instance CategoryTheory.equalizerRegular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (g : X ⟶ Y) (h : X ⟶ Y) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)] : CategoryTheory.RegularMono (CategoryTheory.Limits.equalizer.ι g h)

instance CategoryTheory.RegularMono.ofIsSplitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitMono f] : CategoryTheory.RegularMono f

Every split monomorphism is a regular monomorphism.

def CategoryTheory.RegularMono.lift' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {W : C} (f : X ⟶ Y) [CategoryTheory.RegularMono f] (k : W ⟶ Y) (h : CategoryTheory.CategoryStruct.comp k CategoryTheory.RegularMono.left = CategoryTheory.CategoryStruct.comp k CategoryTheory.RegularMono.right) : { l // CategoryTheory.CategoryStruct.comp l f = k }

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.

def CategoryTheory.regularOfIsPullbackSndOfRegular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : C} {Q : C} {R : C} {S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [hr : CategoryTheory.RegularMono h] (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm)) : CategoryTheory.RegularMono g

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.

def CategoryTheory.regularOfIsPullbackFstOfRegular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : C} {Q : C} {R : C} {S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [CategoryTheory.RegularMono k] (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm)) : CategoryTheory.RegularMono f

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.

instance CategoryTheory.strongMono_of_regularMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.RegularMono f] : CategoryTheory.StrongMono f

theorem CategoryTheory.isIso_of_regularMono_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.RegularMono f] [CategoryTheory.Epi f] : CategoryTheory.IsIso f

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

class CategoryTheory.RegularMonoCategory (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Type (max u₁ v₁)

• regularMonoOfMono : {X Y : C} → (f : X ⟶ Y) → [inst : CategoryTheory.Mono f] → CategoryTheory.RegularMono f

  Every monomorphism is a regular monomorphism

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

def CategoryTheory.regularMonoOfMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.RegularMonoCategory C] (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.RegularMono f

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.

instance CategoryTheory.regularMonoCategoryOfSplitMonoCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitMonoCategory C] : CategoryTheory.RegularMonoCategory C

instance CategoryTheory.strongMonoCategory_of_regularMonoCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.RegularMonoCategory C] : CategoryTheory.StrongMonoCategory C

class CategoryTheory.RegularEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) : Type (max u₁ v₁)

• W : C

  An object from C

• left : CategoryTheory.RegularEpi.W f ⟶ X

  Two maps to the domain of f

• right : CategoryTheory.RegularEpi.W f ⟶ X

  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 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left f = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right f))

  f is the coequalizer

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

theorem CategoryTheory.RegularEpi.w_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {f : X ⟶ Y} [self : CategoryTheory.RegularEpi f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right (CategoryTheory.CategoryStruct.comp f h)

instance CategoryTheory.RegularEpi.epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.RegularEpi f] : CategoryTheory.Epi f

Every regular epimorphism is an epimorphism.

instance CategoryTheory.coequalizerRegular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (g : X ⟶ Y) (h : X ⟶ Y) [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair g h)] : CategoryTheory.RegularEpi (CategoryTheory.Limits.coequalizer.π g h)

instance CategoryTheory.RegularEpi.ofSplitEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitEpi f] : CategoryTheory.RegularEpi f

Every split epimorphism is a regular epimorphism.

def CategoryTheory.RegularEpi.desc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {W : C} (f : X ⟶ Y) [CategoryTheory.RegularEpi f] (k : X ⟶ W) (h : CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left k = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right k) : { l // CategoryTheory.CategoryStruct.comp f l = k }

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.

def CategoryTheory.regularOfIsPushoutSndOfRegular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : C} {Q : C} {R : C} {S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [gr : CategoryTheory.RegularEpi g] (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) (t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm)) : CategoryTheory.RegularEpi h

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.

def CategoryTheory.regularOfIsPushoutFstOfRegular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : C} {Q : C} {R : C} {S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [CategoryTheory.RegularEpi f] (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) (t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm)) : CategoryTheory.RegularEpi k

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.

instance CategoryTheory.strongEpi_of_regularEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.RegularEpi f] : CategoryTheory.StrongEpi f

theorem CategoryTheory.isIso_of_regularEpi_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.RegularEpi f] [CategoryTheory.Mono f] : CategoryTheory.IsIso f

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

class CategoryTheory.RegularEpiCategory (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Type (max u₁ v₁)

• regularEpiOfEpi : {X Y : C} → (f : X ⟶ Y) → [inst : CategoryTheory.Epi f] → CategoryTheory.RegularEpi f

  Everyone epimorphism is a regular epimorphism

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

def CategoryTheory.regularEpiOfEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.RegularEpiCategory C] (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.RegularEpi f

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.

instance CategoryTheory.regularEpiCategoryOfSplitEpiCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitEpiCategory C] : CategoryTheory.RegularEpiCategory C

instance CategoryTheory.strongEpiCategory_of_regularEpiCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.RegularEpiCategory C] : CategoryTheory.StrongEpiCategory C