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

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] : Nonempty (RegularMono 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 = ⋯.some

@[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.

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.

@[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)

@[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] : Nonempty (RegularEpi 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 = ⋯.some

@[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