Split coequalizers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
In addition, we show that every split coequalizer is a coequalizer
category_theory.is_split_coequalizer.is_coequalizer) and absolute
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.
- right_section : Z ⟶ Y
- left_section : Y ⟶ X
- condition : f ≫ π = g ≫ π
- right_section_π : self.right_section ≫ π = 𝟙 Z
- left_section_top : self.left_section ≫ f = π ≫ self.right_section
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.
A split coequalizer clearly induces a cofork.
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.
f,g is a split pair if there is a
h : Y ⟶ Z so that
f, g, h forms a split coequalizer
Instances of this typeclass
Get the coequalizer object from the typeclass
Get the coequalizer morphism from the typeclass
The coequalizer morphism
coequalizer_ι gives a split coequalizer on
f, g is split, then
G f, G g is split.
If a pair has a split coequalizer, it has a coequalizer.