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
andRegularMono → Mono
as well as the dual constructions for regular epimorphisms. Additionally, we give the constructionRegularEpi ⟶ StrongEpi
.
We also define classes RegularMonoCategory
and RegularEpiCategory
for categories in which
every monomorphism or epimorphism is regular, and deduce that these categories are
StrongMonoCategory
s resp. StrongEpiCategory
s.
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
toZ
- right : Y ⟶ CategoryTheory.RegularMono.Z f
Another map from the codomain of
f
toZ
- 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
Instances
Every regular monomorphism is a monomorphism.
Equations
- One or more equations did not get rendered due to their size.
Every split monomorphism is a regular monomorphism.
Equations
- One or more equations did not get rendered due to their size.
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
Instances For
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.
Instances For
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
Instances For
A regular monomorphism is an isomorphism if it is an epimorphism.
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
Instances
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
Instances For
Equations
- CategoryTheory.regularMonoCategoryOfSplitMonoCategory = { regularMonoOfMono := fun {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.Mono f) => inferInstance }
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
Instances
Every regular epimorphism is an epimorphism.
Equations
- One or more equations did not get rendered due to their size.
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.
Instances For
Every split epimorphism is a regular epimorphism.
Equations
- One or more equations did not get rendered due to their size.
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
Instances For
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.
Instances For
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
Instances For
A regular epimorphism is an isomorphism if it is a monomorphism.
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
Instances
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.
Instances For
Equations
- CategoryTheory.regularEpiCategoryOfSplitEpiCategory = { regularEpiOfEpi := fun {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.Epi f) => inferInstance }