# 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
Instances for category_theory.monad.free_coequalizer.top_map

The bottom map in the coequalizer diagram we will construct.

Equations
Instances for category_theory.monad.free_coequalizer.bottom_map
@[simp]

The cofork map in the coequalizer diagram we will construct.

Equations
@[protected, 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_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
@[simp]
theorem category_theory.monad.beck_cofork_π {C : Type u₁} {T : category_theory.monad C} (X : T.algebra) :

The Beck cofork is a coequalizer.

Equations
@[simp]
theorem category_theory.monad.beck_coequalizer_desc {C : Type u₁} {T : category_theory.monad C} (X : T.algebra) (s : (T.μ.app X.A)) :
= T.η.app X.A s.π