mathlib documentation

category_theory.monad.coequalizer

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.

Equations

The cofork map in the coequalizer diagram we will construct.

Equations
@[simp]
theorem category_theory.monad.beck_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_cofork X).ι.app X_1 = category_theory.limits.walking_parallel_pair.rec (T.map X.a X.a) X.a X_1

This is the Beck cofork. It is a split coequalizer, in particular a coequalizer.

Equations