Split Equalizers #
We define what it means for a triple of morphisms f g : X ⟶ Y
, ι : W ⟶ X
to be a split
equalizer: there is a retraction r
of ι
and a retraction t
of g
, which additionally satisfy
t ≫ f = r ≫ ι
.
In addition, we show that every split equalizer is an equalizer
(CategoryTheory.IsSplitEqualizer.isEqualizer
) and absolute
(CategoryTheory.IsSplitEqualizer.map
)
A pair f g : X ⟶ Y
has a split equalizer if there is a W
and ι : W ⟶ X
making f,g,ι
a
split equalizer.
A pair f g : X ⟶ Y
has a G
-split equalizer if G f, G g
has a split equalizer.
These definitions and constructions are useful in particular for the comonadicity theorems.
This file was adapted from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
. Please try
to keep them in sync.
A split equalizer diagram consists of morphisms
ι f
W → X ⇉ Y
g
satisfying ι ≫ f = ι ≫ g
together with morphisms
r t
W ← X ← Y
satisfying ι ≫ r = 𝟙 W
, g ≫ t = 𝟙 X
and f ≫ t = r ≫ ι
.
The name "equalizer" is appropriate, since any split equalizer is a equalizer, see
CategoryTheory.IsSplitEqualizer.isEqualizer
.
Split equalizers are also absolute, since a functor preserves all the structure above.
- leftRetraction : X ⟶ W
A map from
X
to the equalizer - rightRetraction : Y ⟶ X
A map in the opposite direction to
f
andg
- condition : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g
Composition of
ι
withf
and withg
agree - ι_leftRetraction : CategoryTheory.CategoryStruct.comp ι self.leftRetraction = CategoryTheory.CategoryStruct.id W
leftRetraction
splitsι
- bottom_rightRetraction : CategoryTheory.CategoryStruct.comp g self.rightRetraction = CategoryTheory.CategoryStruct.id X
rightRetraction
splitsg
- top_rightRetraction : CategoryTheory.CategoryStruct.comp f self.rightRetraction = CategoryTheory.CategoryStruct.comp self.leftRetraction ι
f
composed withrightRetraction
isleftRetraction
composed withι
Instances For
Equations
- One or more equations did not get rendered due to their size.
Split equalizers are absolute: they are preserved by any functor.
Equations
- q.map F = { leftRetraction := F.map q.leftRetraction, rightRetraction := F.map q.rightRetraction, condition := ⋯, ι_leftRetraction := ⋯, bottom_rightRetraction := ⋯, top_rightRetraction := ⋯ }
Instances For
A split equalizer clearly induces a fork.
Equations
- t.asFork = CategoryTheory.Limits.Fork.ofι h ⋯
Instances For
The fork induced by a split equalizer is an equalizer, justifying the name. In some cases it is more convenient to show a given fork is an equalizer by showing it is split.
Equations
- t.isEqualizer = CategoryTheory.Limits.Fork.IsLimit.mk' t.asFork fun (s : CategoryTheory.Limits.Fork f g) => ⟨CategoryTheory.CategoryStruct.comp s.ι t.leftRetraction, ⋯⟩
Instances For
The pair f,g
is a cosplit pair if there is an h : W ⟶ X
so that f, g, h
forms a split
equalizer in C
.
- splittable : ∃ (W : C) (h : W ⟶ X), Nonempty (CategoryTheory.IsSplitEqualizer f g h)
There is some split equalizer
Instances
The pair f,g
is a G
-cosplit pair if there is an h : W ⟶ G X
so that G f, G g, h
forms a
split equalizer in D
.
Equations
- G.IsCosplitPair f g = CategoryTheory.HasSplitEqualizer (G.map f) (G.map g)
Instances For
Get the equalizer object from the typeclass IsCosplitPair
.
Equations
- CategoryTheory.HasSplitEqualizer.equalizerOfSplit f g = ⋯.choose
Instances For
Get the equalizer morphism from the typeclass IsCosplitPair
.
Equations
- CategoryTheory.HasSplitEqualizer.equalizerι f g = ⋯.choose
Instances For
The equalizer morphism equalizerι
gives a split equalizer on f,g
.
Equations
Instances For
If f, g
is cosplit, then G f, G g
is cosplit.
If a pair has a split equalizer, it has a equalizer.