Split coequalizers #
We define what it means for a triple of morphisms
f g : X ⟶ Y,
π : Y ⟶ Z to be a split
coequalizer: there is a section
π and a section
g, which additionally satisfy
t ≫ f = π ≫ s.
f g : X ⟶ Y has a split coequalizer if there is a
π : Y ⟶ Z making
f g : X ⟶ Y has a
G-split coequalizer if
G f, G g has a split coequalizer.
These definitions and constructions are useful in particular for the monadicity theorems.
Dualise to split equalizers.
- rightSection : Z ⟶ Y
A map from the coequalizer to
- leftSection : Y ⟶ X
A map in the opposite direction to
- rightSection_π : CategoryTheory.CategoryStruct.comp s.rightSection π = CategoryTheory.CategoryStruct.id Z
- leftSection_top : CategoryTheory.CategoryStruct.comp s.leftSection f = CategoryTheory.CategoryStruct.comp π s.rightSection
A split coequalizer diagram consists of morphisms
f π X ⇉ Y → Z g
f ≫ π = g ≫ π together with morphisms
t s X ← Y ← Z
s ≫ π = 𝟙 Z,
t ≫ g = 𝟙 Y and
t ≫ f = π ≫ s.
The name "coequalizer" is appropriate, since any split coequalizer is a coequalizer, see
Split coequalizers are also absolute, since a functor preserves all the structure above.
Split coequalizers are absolute: they are preserved by any functor.
The cofork induced by a split coequalizer is a coequalizer, justifying the name. In some cases it is more convenient to show a given cofork is a coequalizer by showing it is split.
There is some split coequalizer
f,g is a split pair if there is an
h : Y ⟶ Z so that
f, g, h forms a split
f,g is a
G-split pair if there is an
h : G Y ⟶ Z so that
G f, G g, h forms a split
Get the coequalizer morphism from the typeclass
The coequalizer morphism
coequalizeπ gives a split coequalizer on
f, g is split, then
G f, G g is split.