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.
The top map in the coequalizer diagram we will construct.
Equations
The bottom map in the coequalizer diagram we will construct.
The cofork map in the coequalizer diagram we will construct.
Construct the Beck cofork in the category of algebras. This cofork is reflexive as well as a coequalizer.
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' := _}, _⟩)
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 := _}
This is the Beck cofork. It is a split coequalizer, in particular a coequalizer.
The Beck cofork is a coequalizer.