mathlib3 documentation

category_theory.monad.coequalizer

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

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

Equations