Special coequalizers associated to a monad #
Associated to a monad T : C ⥤ C we have important coequalizer constructions:
Any algebra is a coequalizer (in the category of algebras) of free algebras. Furthermore, this
coequalizer is reflexive.
In C, this cofork diagram is a split coequalizer (in particular, it is still a coequalizer).
This split coequalizer is known as the Beck coequalizer (as it features heavily in Beck's
monadicity theorem).
Show that any algebra is a coequalizer of free algebras.
@[simp]
theorem
category_theory.monad.free_coequalizer.top_map_f
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
def
category_theory.monad.free_coequalizer.top_map
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
The top map in the coequalizer diagram we will construct.
Equations
Instances for category_theory.monad.free_coequalizer.top_map
def
category_theory.monad.free_coequalizer.bottom_map
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
The bottom map in the coequalizer diagram we will construct.
Instances for category_theory.monad.free_coequalizer.bottom_map
@[simp]
theorem
category_theory.monad.free_coequalizer.bottom_map_f
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
@[simp]
theorem
category_theory.monad.free_coequalizer.π_f
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
def
category_theory.monad.free_coequalizer.π
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
The cofork map in the coequalizer diagram we will construct.
theorem
category_theory.monad.free_coequalizer.condition
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
@[protected, instance]
def
category_theory.monad.free_coequalizer.bottom_map.category_theory.is_reflexive_pair
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
@[simp]
theorem
category_theory.monad.beck_algebra_cofork_ι_app
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra)
(X_1 : category_theory.limits.walking_parallel_pair) :
(category_theory.monad.beck_algebra_cofork X).ι.app X_1 = category_theory.limits.walking_parallel_pair.rec (category_theory.monad.free_coequalizer.top_map X ≫ category_theory.monad.free_coequalizer.π X) (category_theory.monad.free_coequalizer.π X) X_1
@[simp]
theorem
category_theory.monad.beck_algebra_cofork_X
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
def
category_theory.monad.beck_algebra_cofork
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
Construct the Beck cofork in the category of algebras. This cofork is reflexive as well as a coequalizer.
def
category_theory.monad.beck_algebra_coequalizer
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
The cofork constructed is a colimit. This shows that any algebra is a (reflexive) coequalizer of free algebras.
Equations
- category_theory.monad.beck_algebra_coequalizer X = category_theory.limits.cofork.is_colimit.mk' (category_theory.monad.beck_algebra_cofork X) (λ (s : category_theory.limits.cofork (category_theory.monad.free_coequalizer.top_map X) (category_theory.monad.free_coequalizer.bottom_map X)), ⟨{f := T.η.app (category_theory.monad.beck_algebra_cofork X).X.A ≫ s.π.f, h' := _}, _⟩)
def
category_theory.monad.beck_split_coequalizer
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
category_theory.is_split_coequalizer (T.to_functor.map X.a) (T.μ.app X.A) X.a
The Beck cofork is a split coequalizer.
Equations
- category_theory.monad.beck_split_coequalizer X = {right_section := T.η.app X.A, left_section := T.η.app (T.to_functor.obj X.A), condition := _, right_section_π := _, left_section_bottom := _, left_section_top := _}
@[simp]
theorem
category_theory.monad.beck_cofork_X
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
(category_theory.monad.beck_cofork X).X = X.A
def
category_theory.monad.beck_cofork
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
category_theory.limits.cofork (T.to_functor.map X.a) (T.μ.app X.A)
This is the Beck cofork. It is a split coequalizer, in particular a coequalizer.
@[simp]
theorem
category_theory.monad.beck_cofork_π
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
(category_theory.monad.beck_cofork X).π = X.a
def
category_theory.monad.beck_coequalizer
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra) :
The Beck cofork is a coequalizer.
@[simp]
theorem
category_theory.monad.beck_coequalizer_desc
{C : Type u₁}
[category_theory.category C]
{T : category_theory.monad C}
(X : T.algebra)
(s : category_theory.limits.cofork (T.to_functor.map X.a) (T.μ.app X.A)) :