Definitions and basic properties of regular monomorphisms and epimorphisms.

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

In this file, we give the following definitions.

• RegularMono f, which is a class carrying the data that exhibits f as a regular monomorphism. That is, it carries a fork and data specifying f a the equalizer of that fork.
• IsRegularMono f, which is a proposition stating that f is a regular monomorphism. In particular, this doesn't carry any data. and constructions
• IsSplitMono f → RegularMono f and
• RegularMono f → Mono f as well as the dual definitions/constructions for regular epimorphisms.

Additionally, we give the constructions

• RegularEpi f → EffectiveEpi f, from which it can be deduced that regular epimorphisms are strong.
• regularEpiOfEffectiveEpi: constructs a RegularEpi f instance from EffectiveEpi f and HasPullback f f.

We also define classes IsRegularMonoCategory and IsRegularEpiCategory 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₁} [Category.{v₁, u₁} C] {X 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 : Y ⟶ Z f

  A map from the codomain of f to Z

• right : Y ⟶ Z f

  Another map from the codomain of f to Z

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

  f equalizes the two maps

• isLimit : Limits.IsLimit (Limits.Fork.ofι f ⋯)

  f is the equalizer of the two maps

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

@[instance 100]

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

Every regular monomorphism is a monomorphism.

def CategoryTheory.RegularMono.ofIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) : RegularMono e.hom

Every isomorphism is a regular monomorphism.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.RegularMono.ofArrowIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk g) [h : RegularMono f] : RegularMono g

Regular monomorphisms are preserved by isomorphisms in the arrow category.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.IsRegularMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Prop

IsRegularMono f is the assertion that f is a regular monomorphism.

Equations

• CategoryTheory.IsRegularMono f = Nonempty (CategoryTheory.RegularMono f)

def CategoryTheory.MorphismProperty.regularMono (C : Type u₁) [Category.{v₁, u₁} C] : MorphismProperty C

The MorphismProperty C satisfied by regular monomorphisms in C.

Equations

• CategoryTheory.MorphismProperty.regularMono C f = CategoryTheory.IsRegularMono f

@[simp]

theorem CategoryTheory.MorphismProperty.regularMono_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : regularMono C f ↔ IsRegularMono f

instance CategoryTheory.MorphismProperty.regularMono.containsIdentities {C : Type u₁} [Category.{v₁, u₁} C] : (regularMono C).ContainsIdentities

instance CategoryTheory.MorphismProperty.regularMono.respectsIso {C : Type u₁} [Category.{v₁, u₁} C] : (regularMono C).RespectsIso

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

def CategoryTheory.regularMonoOfIsRegularMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [h : IsRegularMono f] : RegularMono f

Given IsRegularMono f, a choice of data for RegularMono f.

Equations

• CategoryTheory.regularMonoOfIsRegularMono f = Nonempty.some h

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

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

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

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₁} [Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y) [RegularMono f] (k : W ⟶ Y) (h : CategoryStruct.comp k left = CategoryStruct.comp k right) : { l : W ⟶ X // 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.

Equations

• CategoryTheory.RegularMono.lift' f k h = CategoryTheory.Limits.Fork.IsLimit.lift' CategoryTheory.RegularMono.isLimit k h

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.regularOfIsPullbackFstOfRegular comm t = CategoryTheory.regularOfIsPullbackSndOfRegular ⋯ (CategoryTheory.Limits.PullbackCone.flipIsLimit t)

@[instance 100]

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

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

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

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

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

• regularMonoOfMono {X Y : C} (f : X ⟶ Y) [Mono f] : IsRegularMono f

  Every monomorphism is a regular monomorphism

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

Equations

• CategoryTheory.regularMonoOfMono f = CategoryTheory.regularMonoOfIsRegularMono f

@[instance 100]

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

@[instance 100]

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

class CategoryTheory.RegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X 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 : W f ⟶ X

  Two maps to the domain of f

• right : W f ⟶ X

  Two maps to the domain of f

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

  f coequalizes the two maps

• isColimit : Limits.IsColimit (Limits.Cofork.ofπ f ⋯)

  f is the coequalizer

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

@[instance 100]

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

Every regular epimorphism is an epimorphism.

def CategoryTheory.RegularEpi.ofIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) : RegularEpi e.hom

Every isomorphism is a regular epimorphism.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.RegularEpi.ofArrowIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk g) [h : RegularEpi f] : RegularEpi g

Regular epimorphisms are preserved by isomorphisms in the arrow category.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.IsRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Prop

IsRegularEpi f is the assertion that f is a regular epimorphism.

Equations

• CategoryTheory.IsRegularEpi f = Nonempty (CategoryTheory.RegularEpi f)

def CategoryTheory.MorphismProperty.regularEpi (C : Type u₁) [Category.{v₁, u₁} C] : MorphismProperty C

The MorphismProperty C satisfied by regular epimorphisms in C.

Equations

• CategoryTheory.MorphismProperty.regularEpi C f = CategoryTheory.IsRegularEpi f

@[simp]

theorem CategoryTheory.MorphismProperty.regularEpi_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : regularEpi C f ↔ IsRegularEpi f

instance CategoryTheory.MorphismProperty.regularEpi.containsIdentities {C : Type u₁} [Category.{v₁, u₁} C] : (regularEpi C).ContainsIdentities

instance CategoryTheory.MorphismProperty.regularEpi.respectsIso {C : Type u₁} [Category.{v₁, u₁} C] : (regularEpi C).RespectsIso

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

def CategoryTheory.regularEpiOfIsRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [h : IsRegularEpi f] : RegularEpi f

Given IsRegularEpi f, a choice of data for RegularEpi f.

Equations

• CategoryTheory.regularEpiOfIsRegularEpi f = Nonempty.some h

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.regularEpiOfKernelPair {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [Limits.HasPullback f f] (hc : Limits.IsColimit (Limits.Cofork.ofπ f ⋯)) : RegularEpi f

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.

def CategoryTheory.effectiveEpiStructOfRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [RegularEpi f] : EffectiveEpiStruct f

The data of an EffectiveEpi structure on a RegularEpi.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instEffectiveEpiOfRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [RegularEpi f] : EffectiveEpi f

theorem CategoryTheory.effectiveEpi_of_kernelPair {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [Limits.HasPullback f f] (hc : Limits.IsColimit (Limits.Cofork.ofπ f ⋯)) : EffectiveEpi f

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

@[deprecated CategoryTheory.effectiveEpi_of_kernelPair (since := "2025-11-20")]

theorem CategoryTheory.effectiveEpiOfKernelPair {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [Limits.HasPullback f f] (hc : Limits.IsColimit (Limits.Cofork.ofπ f ⋯)) : EffectiveEpi f

Alias of CategoryTheory.effectiveEpi_of_kernelPair.

---

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

noncomputable instance CategoryTheory.regularEpiOfEffectiveEpi {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [Limits.HasPullback f f] [EffectiveEpi f] : RegularEpi f

An effective epi which has a kernel pair is a regular epi.

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

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

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₁} [Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y) [RegularEpi f] (k : X ⟶ W) (h : CategoryStruct.comp left k = CategoryStruct.comp right k) : { l : Y ⟶ W // 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.

Equations

• CategoryTheory.RegularEpi.desc' f k h = CategoryTheory.Limits.Cofork.IsColimit.desc' CategoryTheory.RegularEpi.isColimit k h

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.regularOfIsPushoutFstOfRegular comm t = CategoryTheory.regularOfIsPushoutSndOfRegular ⋯ (CategoryTheory.Limits.PushoutCocone.flipIsColimit t)

@[deprecated "No replacement" (since := "2025-11-20"), instance 100]

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

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

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

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

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

• regularEpiOfEpi {X Y : C} (f : X ⟶ Y) [Epi f] : IsRegularEpi f

  Everyone epimorphism is a regular epimorphism

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

Equations

• CategoryTheory.regularEpiOfEpi f = CategoryTheory.regularEpiOfIsRegularEpi f

@[instance 100]

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

@[instance 100]

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