# 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 CategoryTheory.Monad.FreeCoequalizer.topMap_f {C : Type u₁} [] {T : } (X : ) :
= T.map X.a
def CategoryTheory.Monad.FreeCoequalizer.topMap {C : Type u₁} [] {T : } (X : ) :
().obj (T.obj X.A) ().obj X.A

The top map in the coequalizer diagram we will construct.

Instances For
@[simp]
theorem CategoryTheory.Monad.FreeCoequalizer.bottomMap_f {C : Type u₁} [] {T : } (X : ) :
= ().app X.A
def CategoryTheory.Monad.FreeCoequalizer.bottomMap {C : Type u₁} [] {T : } (X : ) :
().obj (T.obj X.A) ().obj X.A

The bottom map in the coequalizer diagram we will construct.

Instances For
@[simp]
theorem CategoryTheory.Monad.FreeCoequalizer.π_f {C : Type u₁} [] {T : } (X : ) :
def CategoryTheory.Monad.FreeCoequalizer.π {C : Type u₁} [] {T : } (X : ) :
().obj X.A X

The cofork map in the coequalizer diagram we will construct.

Instances For
@[simp]
@[simp]
theorem CategoryTheory.Monad.beckAlgebraCofork_pt {C : Type u₁} [] {T : } (X : ) :

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

Instances For

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

Instances For
def CategoryTheory.Monad.beckSplitCoequalizer {C : Type u₁} [] {T : } (X : ) :
CategoryTheory.IsSplitCoequalizer (T.map X.a) (().app X.A) X.a

The Beck cofork is a split coequalizer.

Instances For
@[simp]
theorem CategoryTheory.Monad.beckCofork_pt {C : Type u₁} [] {T : } (X : ) :
= X.A
def CategoryTheory.Monad.beckCofork {C : Type u₁} [] {T : } (X : ) :
CategoryTheory.Limits.Cofork (T.map X.a) (().app X.A)

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

Instances For
@[simp]
theorem CategoryTheory.Monad.beckCofork_π {C : Type u₁} [] {T : } (X : ) :

The Beck cofork is a coequalizer.

Instances For
@[simp]
theorem CategoryTheory.Monad.beckCoequalizer_desc {C : Type u₁} [] {T : } (X : ) (s : CategoryTheory.Limits.Cofork (T.map X.a) (().app X.A)) :