# Special coequalizers associated to a monad #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
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

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

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

The Beck cofork is a split coequalizer.

Equations
@[simp]
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]

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.π