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 s
of π
and a section t
of 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
(category_theory.is_split_coequalizer.map
)
A pair f g : X ⟶ Y
has a split coequalizer if there is a Z
and π : Y ⟶ Z
making f,g,π
a
split coequalizer.
A pair 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.
TODO #
Dualise to split equalizers.
- right_section : Z ⟶ Y
- left_section : Y ⟶ X
- condition : f ≫ π = g ≫ π
- right_section_π : self.right_section ≫ π = 𝟙 Z
- left_section_bottom : self.left_section ≫ g = 𝟙 Y
- left_section_top : self.left_section ≫ f = π ≫ self.right_section
A split coequalizer diagram consists of morphisms
f π
X ⇉ Y → Z
g
satisfying f ≫ π = g ≫ π
together with morphisms
t s
X ← Y ← Z
satisfying s ≫ π = 𝟙 Z
, t ≫ g = 𝟙 Y
and t ≫ f = π ≫ s
.
The name "coequalizer" is appropriate, since any split coequalizer is a coequalizer, see
category_theory.is_split_coequalizer.is_coequalizer
.
Split coequalizers are also absolute, since a functor preserves all the structure above.
Instances for category_theory.is_split_coequalizer
- category_theory.is_split_coequalizer.has_sizeof_inst
- category_theory.is_split_coequalizer.inhabited
Equations
- category_theory.is_split_coequalizer.inhabited = {default := {right_section := 𝟙 X, left_section := 𝟙 X, condition := _, right_section_π := _, left_section_bottom := _, left_section_top := _}}
Split coequalizers are absolute: they are preserved by any functor.
Equations
- q.map F = {right_section := F.map q.right_section, left_section := F.map q.left_section, condition := _, right_section_π := _, left_section_bottom := _, left_section_top := _}
A split coequalizer clearly induces a cofork.
Equations
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.
Equations
- t.is_coequalizer = category_theory.limits.cofork.is_colimit.mk' t.as_cofork (λ (s : category_theory.limits.cofork f g), ⟨t.right_section ≫ s.π, _⟩)
- splittable : ∃ {Z : C} (h : Y ⟶ Z), nonempty (category_theory.is_split_coequalizer f g h)
The pair f,g
is a split pair if there is a h : Y ⟶ Z
so that f, g, h
forms a split coequalizer
in C
.
Instances of this typeclass
The pair f,g
is a G
-split pair if there is a h : G Y ⟶ Z
so that G f, G g, h
forms a split
coequalizer in D
.
Get the coequalizer object from the typeclass is_split_pair
.
Equations
Get the coequalizer morphism from the typeclass is_split_pair
.
Equations
The coequalizer morphism coequalizer_ι
gives a split coequalizer on f,g
.
If f, g
is split, then G f, G g
is split.
If a pair has a split coequalizer, it has a coequalizer.