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]

The top map in the coequalizer diagram we will construct.

Equations

The bottom map in the coequalizer diagram we will construct.

Equations
@[simp]

The cofork map in the coequalizer diagram we will construct.

Equations
@[instance]
@[simp]
theorem category_theory.monad.beck_algebra_cofork_ι_app {C : Type u₁} {T : category_theory.monad C} (X : T.algebra)  :
= category_theory.limits.walking_parallel_pair.rec X_1
@[simp]

Construct the Beck cofork in the category of algebras. This cofork is reflexive as well as a coequalizer.

Equations

The cofork constructed is a colimit. This shows that any algebra is a (reflexive) coequalizer of free algebras.

Equations
def category_theory.monad.beck_split_coequalizer {C : Type u₁} {T : category_theory.monad C} (X : T.algebra) :
(T.μ.app X.A) X.a

The Beck cofork is a split coequalizer.

Equations
@[simp]
theorem category_theory.monad.beck_cofork_ι_app {C : Type u₁} {T : category_theory.monad C} (X : T.algebra)  :
= category_theory.limits.walking_parallel_pair.rec (T.map X.a X.a) X.a X_1
@[simp]
theorem category_theory.monad.beck_cofork_X {C : Type u₁} {T : category_theory.monad C} (X : T.algebra) :
def category_theory.monad.beck_cofork {C : Type u₁} {T : category_theory.monad C} (X : T.algebra) :
(T.μ.app X.A)

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

Equations

The Beck cofork is a coequalizer.

Equations