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 structure carrying the data that exhibits f as a regular monomorphism. That is, it carries a fork and data specifying f as the equalizer of that fork.
• IsRegularMono f, which is a Prop-valued class 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.

structure 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 ⟶ self.Z

  A map from the codomain of f to Z

• right : Y ⟶ self.Z

  Another map from the codomain of f to Z

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

f equalizes the two maps

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

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

• regularMono : Nonempty (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

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

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

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

Equations

• CategoryTheory.IsRegularMono.getStruct f = ⋯.some

@[deprecated CategoryTheory.IsRegularMono.getStruct (since := "2025-12-01")]

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

Alias of CategoryTheory.IsRegularMono.getStruct.

---

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

Equations

• @CategoryTheory.regularMonoOfIsRegularMono = @CategoryTheory.IsRegularMono.getStruct

def CategoryTheory.Fork.IsLimit.regularMono {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} {p₁ p₂ : A ⟶ B} {c : Limits.Fork p₁ p₂} (h : Limits.IsLimit c) : RegularMono c.ι

An equalizer diagram gives rise to a regular monomorphism.

Equations

• CategoryTheory.Fork.IsLimit.regularMono h = { Z := B, left := p₁, right := p₂, w := ⋯, isLimit := h.ofIsoLimit c.isoForkOfι }

Given a regular monomorphism f : X ⟶ Y (i.e. a morphism satisfying the predicate IsRegularMono), this section gives an equalizer diagram

     X
    f|
     v
     Y
left| |right
    v v
     Z

The names Z, left, and right all being in the IsRegularMono namespace.

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

The target of the equalizer diagram for f.

Equations

• CategoryTheory.IsRegularMono.Z f = (CategoryTheory.IsRegularMono.getStruct f).Z

noncomputable def CategoryTheory.IsRegularMono.left {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularMono f] : Y ⟶ Z f

The "left" map Y ⟶ Z.

Equations

• CategoryTheory.IsRegularMono.left f = (CategoryTheory.IsRegularMono.getStruct f).left

noncomputable def CategoryTheory.IsRegularMono.right {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularMono f] : Y ⟶ Z f

The "right" map Y ⟶ Z.

Equations

• CategoryTheory.IsRegularMono.right f = (CategoryTheory.IsRegularMono.getStruct f).right

theorem CategoryTheory.IsRegularMono.w {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularMono f] : CategoryStruct.comp f (left f) = CategoryStruct.comp f (right f)

The equalizer condition.

noncomputable def CategoryTheory.IsRegularMono.isLimit {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularMono f] : Limits.IsLimit (Limits.Fork.ofι f ⋯)

The fork is in fact an equalizer.

Equations

• CategoryTheory.IsRegularMono.isLimit f = (CategoryTheory.IsRegularMono.getStruct f).isLimit

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

Lift a morphism k : W ⟶ Y, equalized by the two morphisms left and right, along f.

Equations

• CategoryTheory.IsRegularMono.lift f k h = CategoryTheory.Limits.Fork.IsLimit.lift (CategoryTheory.IsRegularMono.isLimit f) k h

@[simp]

theorem CategoryTheory.IsRegularMono.fac {C : Type u₁} [Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y) [IsRegularMono f] (k : W ⟶ Y) (h : CategoryStruct.comp k (left f) = CategoryStruct.comp k (right f)) : CategoryStruct.comp (lift f k h) f = k

@[simp]

theorem CategoryTheory.IsRegularMono.fac_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y) [IsRegularMono f] (k : W ⟶ Y) (h : CategoryStruct.comp k (left f) = CategoryStruct.comp k (right f)) {Z : C} (h✝ : Y ⟶ Z) : CategoryStruct.comp (lift f k h) (CategoryStruct.comp f h✝) = CategoryStruct.comp k h✝

theorem CategoryTheory.IsRegularMono.uniq {C : Type u₁} [Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y) [IsRegularMono f] (k : W ⟶ Y) (h : CategoryStruct.comp k (left f) = CategoryStruct.comp k (right f)) (m : W ⟶ X) (hm : CategoryStruct.comp m f = k) : m = lift f k h

noncomputable def CategoryTheory.RegularMono.equalizer {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)

The chosen equalizer of a parallel pair is a regular monomorphism.

Equations

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

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

noncomputable def 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.

@[instance 100]

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

def CategoryTheory.RegularMono.lift' {C : Type u₁} [Category.{v₁, u₁} C] {X Y W : C} {f : X ⟶ Y} (hf : RegularMono f) (k : W ⟶ Y) (h : CategoryStruct.comp k hf.left = CategoryStruct.comp k hf.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

• hf.lift' k h = CategoryTheory.Limits.Fork.IsLimit.lift' hf.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} (hk : 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 hk comm t = CategoryTheory.regularOfIsPullbackSndOfRegular hk ⋯ (CategoryTheory.Limits.PullbackCone.flipIsLimit t)

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

Any regular monomorphism is a strong monomorphism.

@[instance 100]

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

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

noncomputable 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.IsRegularMono.getStruct 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

structure 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 : self.W ⟶ X

  Two maps to the domain of f

• right : self.W ⟶ X

  Two maps to the domain of f

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

f coequalizes the two maps

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

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

• regularEpi : Nonempty (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

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

noncomputable def CategoryTheory.IsRegularEpi.getStruct {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.IsRegularEpi.getStruct f = ⋯.some

@[deprecated CategoryTheory.IsRegularEpi.getStruct (since := "2025-12-01")]

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

Alias of CategoryTheory.IsRegularEpi.getStruct.

---

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

Equations

• @CategoryTheory.regularEpiOfIsRegularEpi = @CategoryTheory.IsRegularEpi.getStruct

def CategoryTheory.Cofork.IsColimit.regularEpi {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} {p₁ p₂ : A ⟶ B} {c : Limits.Cofork p₁ p₂} (h : Limits.IsColimit c) : RegularEpi c.π

A coequalizer diagram gives rise to a regular epimorphism.

Equations

• CategoryTheory.Cofork.IsColimit.regularEpi h = { W := A, left := p₁, right := p₂, w := ⋯, isColimit := h.ofIsoColimit c.isoCoforkOfπ }

Given a regular epimorphism f : X ⟶ Y (i.e. a morphism satisfying the predicate IsRegularEpi), this section gives a coequalizer diagram

     W
left| |right
    v v
     X
    f|
     v
     Y

The names W, left, and right all being in the IsRegularEpi namespace.

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

The source of the coequalizer diagram for f.

Equations

• CategoryTheory.IsRegularEpi.W f = (CategoryTheory.IsRegularEpi.getStruct f).W

noncomputable def CategoryTheory.IsRegularEpi.left {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularEpi f] : W f ⟶ X

The "left" map W ⟶ X.

Equations

• CategoryTheory.IsRegularEpi.left f = (CategoryTheory.IsRegularEpi.getStruct f).left

noncomputable def CategoryTheory.IsRegularEpi.right {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularEpi f] : W f ⟶ X

The "right" map W ⟶ X.

Equations

• CategoryTheory.IsRegularEpi.right f = (CategoryTheory.IsRegularEpi.getStruct f).right

theorem CategoryTheory.IsRegularEpi.w {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularEpi f] : CategoryStruct.comp (left f) f = CategoryStruct.comp (right f) f

The coequalizer condition.

noncomputable def CategoryTheory.IsRegularEpi.isColimit {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularEpi f] : Limits.IsColimit (Limits.Cofork.ofπ f ⋯)

The cofork is in fact a coequalizer.

Equations

• CategoryTheory.IsRegularEpi.isColimit f = (CategoryTheory.IsRegularEpi.getStruct f).isColimit

noncomputable def CategoryTheory.IsRegularEpi.desc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) [IsRegularEpi f] (k : X ⟶ Z) (h : CategoryStruct.comp (left f) k = CategoryStruct.comp (right f) k) : Y ⟶ Z

Descend a morphism k : X ⟶ Z, coequalized by the two morphisms left and right, along f.

Equations

• CategoryTheory.IsRegularEpi.desc f k h = CategoryTheory.Limits.Cofork.IsColimit.desc (CategoryTheory.IsRegularEpi.isColimit f) k h

@[simp]

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

@[simp]

theorem CategoryTheory.IsRegularEpi.fac_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) [IsRegularEpi f] (k : X ⟶ Z) (h : CategoryStruct.comp (left f) k = CategoryStruct.comp (right f) k) {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryStruct.comp f (CategoryStruct.comp (desc f k h) h✝) = CategoryStruct.comp k h✝

theorem CategoryTheory.IsRegularEpi.uniq {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) [IsRegularEpi f] (k : X ⟶ Z) (h : CategoryStruct.comp (left f) k = CategoryStruct.comp (right f) k) (m : Y ⟶ Z) (hm : CategoryStruct.comp f m = k) : m = desc f k h

noncomputable def 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)

The chosen coequalizer of a parallel pair is a regular epimorphism.

Equations

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

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

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.

theorem CategoryTheory.IsRegularEpi.of_epi_of_exists {C : Type u₁} [Category.{v₁, u₁} C] {X B : C} {f : X ⟶ B} [Limits.HasPullback f f] [Epi f] (h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, CategoryStruct.comp (Limits.pullback.fst f f) g = CategoryStruct.comp (Limits.pullback.snd f f) g → ∃ (u : B ⟶ Z), CategoryStruct.comp f u = g) : IsRegularEpi f

def CategoryTheory.effectiveEpiStructOfRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} {f : X ⟶ B} (hf : 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.

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

@[instance 100]

instance CategoryTheory.instEffectiveEpiOfIsRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} {f : X ⟶ B} [h : IsRegularEpi 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 def CategoryTheory.isColimitCoforkOfEffectiveEpi {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [EffectiveEpi f] (c : Limits.PullbackCone f f) (hc : Limits.IsLimit c) : Limits.IsColimit (Limits.Cofork.ofπ f ⋯)

Given a kernel pair of an effective epimorphism f : X ⟶ B, the induced cofork is a coequalizer.

Equations

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

noncomputable def 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 CategoryTheory.isRegularEpi_of_EffectiveEpi {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [Limits.HasPullback f f] [EffectiveEpi f] : IsRegularEpi f

theorem CategoryTheory.isRegularEpi_iff_effectiveEpi {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [Limits.HasPullback f f] : IsRegularEpi f ↔ EffectiveEpi f

noncomputable def CategoryTheory.EffectiveEpiStruct.isColimitCoforkOfIsPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {p : Y ⟶ X} (hp : EffectiveEpiStruct p) {p₁ p₂ : Z ⟶ Y} (sq : IsPullback p₁ p₂ p p) : Limits.IsColimit (Limits.Cofork.ofπ p ⋯)

Let p : Y ⟶ X be an effective epimorphism, p₁ : Z ⟶ Y and p₂ : Z ⟶ Y two morphisms which make Z the pullback of two copies of Y over X. Then, Y ⟶ X is the coequalizer of p₁ and p₂.

Equations

• hp.isColimitCoforkOfIsPullback sq = CategoryTheory.Limits.Cofork.IsColimit.mk (CategoryTheory.Limits.Cofork.ofπ p ⋯) (fun (s : CategoryTheory.Limits.Cofork p₁ p₂) => hp.desc s.π ⋯) ⋯ ⋯

noncomputable def 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.

@[instance 100]

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

def CategoryTheory.RegularEpi.desc' {C : Type u₁} [Category.{v₁, u₁} C] {X Y W : C} {f : X ⟶ Y} (hf : RegularEpi f) (k : X ⟶ W) (h : CategoryStruct.comp hf.left k = CategoryStruct.comp hf.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

• hf.desc' k h = CategoryTheory.Limits.Cofork.IsColimit.desc' hf.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} (hf : 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 hf comm t = CategoryTheory.regularOfIsPushoutSndOfRegular hf ⋯ (CategoryTheory.Limits.PushoutCocone.flipIsColimit t)

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

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

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

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

noncomputable def CategoryTheory.RegularMono.op {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (hf : RegularMono f) : RegularEpi f.op

A regular monomorphism in C induces a regular epimorphism in Cᵒᵖ.

Equations

• hf.op = { W := Opposite.op hf.Z, left := hf.left.op, right := hf.right.op, w := ⋯, isColimit := (CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitOp f f ⋯ ⋯ ⋯) hf.isLimit }

noncomputable def CategoryTheory.RegularMono.unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f : X ⟶ Y} (hf : RegularMono f) : RegularEpi f.unop

A regular monomorphism in Cᵒᵖ induces a regular epimorphism in C.

Equations

• hf.unop = { W := Opposite.unop hf.Z, left := hf.left.unop, right := hf.right.unop, w := ⋯, isColimit := (CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitUnop f f ⋯ ⋯ ⋯) hf.isLimit }

noncomputable def CategoryTheory.RegularEpi.op {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (hf : RegularEpi f) : RegularMono f.op

A regular epimorphism in C induces a regular monomorphism in Cᵒᵖ.

Equations

• hf.op = { Z := Opposite.op hf.W, left := hf.left.op, right := hf.right.op, w := ⋯, isLimit := (CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp f f ⋯ ⋯ ⋯) hf.isColimit }

noncomputable def CategoryTheory.RegularEpi.unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f : X ⟶ Y} (hf : RegularEpi f) : RegularMono f.unop

A regular epimorphism in Cᵒᵖ induces a regular monomorphism in C.

Equations

• hf.unop = { Z := Opposite.unop hf.W, left := hf.left.unop, right := hf.right.unop, w := ⋯, isLimit := (CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitUnop f f ⋯ ⋯ ⋯) hf.isColimit }

@[simp]

theorem CategoryTheory.isRegularMono_op_iff_isRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : IsRegularMono f.op ↔ IsRegularEpi f

instance CategoryTheory.instIsRegularMonoOppositeOpOfIsRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularEpi f] : IsRegularMono f.op

@[simp]

theorem CategoryTheory.isRegularMono_unop_iff_isRegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : IsRegularMono f.unop ↔ IsRegularEpi f

instance CategoryTheory.instIsRegularMonoUnopOfIsRegularEpiOpposite {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsRegularEpi f] : IsRegularMono f.unop

@[simp]

theorem CategoryTheory.isRegularEpi_op_iff_isRegularMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : IsRegularEpi f.op ↔ IsRegularMono f

instance CategoryTheory.instIsRegularEpiOppositeOpOfIsRegularMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsRegularMono f] : IsRegularEpi f.op

@[simp]

theorem CategoryTheory.isRegularEpi_unop_iff_isRegularMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : IsRegularEpi f.unop ↔ IsRegularMono f

instance CategoryTheory.instIsRegularEpiUnopOfIsRegularMonoOpposite {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsRegularMono f] : IsRegularEpi f.unop

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

noncomputable 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.IsRegularEpi.getStruct 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