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₁)

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

• 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 ⋯)

  f is the equalizer of the two maps

theorem CategoryTheory.RegularMono.w {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.RegularMono f], 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₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X 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 100]

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.

Equations

• ⋯ = ⋯

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)

Equations

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

@[instance 100]

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.

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

@[instance 100]

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

Equations

• ⋯ = ⋯

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₁)

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

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

  Every monomorphism is a regular monomorphism

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.

Equations

• CategoryTheory.regularMonoOfMono f = CategoryTheory.RegularMonoCategory.regularMonoOfMono f

@[instance 100]

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

Equations

• CategoryTheory.regularMonoCategoryOfSplitMonoCategory = { regularMonoOfMono := fun {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.Mono f) => inferInstance }

@[instance 100]

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

Equations

• ⋯ = ⋯

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

  f is the coequalizer

theorem CategoryTheory.RegularEpi.w {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.RegularEpi f], 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₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X 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 100]

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.

Equations

• ⋯ = ⋯

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)

Equations

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

noncomputable def CategoryTheory.regularEpiOfKernelPair {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.Limits.HasPullback f f] (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)) : CategoryTheory.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.

@[instance 100]

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.

Equations

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

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 : Y ⟶ W // 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.

Equations

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

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.

Equations

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

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.

Equations

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

@[instance 100]

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

Equations

• ⋯ = ⋯

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₁)

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

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

  Everyone epimorphism is a regular epimorphism

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.

Equations

• CategoryTheory.regularEpiOfEpi f = CategoryTheory.RegularEpiCategory.regularEpiOfEpi f

@[instance 100]

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

Equations

• CategoryTheory.regularEpiCategoryOfSplitEpiCategory = { regularEpiOfEpi := fun {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.Epi f) => inferInstance }

@[instance 100]

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

Equations

• ⋯ = ⋯