mathlib documentation

category_theory.monad.coequalizer

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.

source
@[simp]
theorem category_theory.monad.free_coequalizer.top_map_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
(category_theory.monad.free_coequalizer.top_map X).f = ↑T.map X.a
source
def category_theory.monad.free_coequalizer.top_map {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
T.free.obj (T.to_functor.obj X.A) ⟶ T.free.obj X.A

The top map in the coequalizer diagram we will construct.

Equations
source
def category_theory.monad.free_coequalizer.bottom_map {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
T.free.obj (T.to_functor.obj X.A) ⟶ T.free.obj X.A

The bottom map in the coequalizer diagram we will construct.

Equations
source
@[simp]
theorem category_theory.monad.free_coequalizer.bottom_map_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
(category_theory.monad.free_coequalizer.bottom_map X).f = T.μ.app X.A
source
@[simp]
theorem category_theory.monad.free_coequalizer.π_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
(category_theory.monad.free_coequalizer.π X).f = X.a
source
def category_theory.monad.free_coequalizer.π {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
T.free.obj X.A ⟶ X

The cofork map in the coequalizer diagram we will construct.

Equations
source
theorem category_theory.monad.free_coequalizer.condition {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
category_theory.monad.free_coequalizer.top_map X ≫ category_theory.monad.free_coequalizer.π X = category_theory.monad.free_coequalizer.bottom_map X ≫ category_theory.monad.free_coequalizer.π X
source
@[instance]
def category_theory.monad.free_coequalizer.bottom_map.category_theory.is_reflexive_pair {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
category_theory.is_reflexive_pair (category_theory.monad.free_coequalizer.top_map X) (category_theory.monad.free_coequalizer.bottom_map X)
source
@[simp]
theorem category_theory.monad.beck_algebra_cofork_ι_app {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) (X_1 : category_theory.limits.walking_parallel_pair) :
(category_theory.monad.beck_algebra_cofork X).ι.app X_1 = category_theory.limits.walking_parallel_pair.rec (category_theory.monad.free_coequalizer.top_map X ≫ category_theory.monad.free_coequalizer.π X) (category_theory.monad.free_coequalizer.π X) X_1
source
@[simp]
theorem category_theory.monad.beck_algebra_cofork_X {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
(category_theory.monad.beck_algebra_cofork X).X = X
source
def category_theory.monad.beck_algebra_cofork {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
category_theory.limits.cofork (category_theory.monad.free_coequalizer.top_map X) (category_theory.monad.free_coequalizer.bottom_map X)

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

Equations
source
def category_theory.monad.beck_algebra_coequalizer {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
category_theory.limits.is_colimit (category_theory.monad.beck_algebra_cofork X)

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

Equations
source
def category_theory.monad.beck_split_coequalizer {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
category_theory.is_split_coequalizer (T.to_functor.map X.a) (T.μ.app X.A) X.a

The Beck cofork is a split coequalizer.

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

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

Equations
source
def category_theory.monad.beck_coequalizer {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (X : T.algebra) :
category_theory.limits.is_colimit (category_theory.monad.beck_cofork X)

The Beck cofork is a coequalizer.

Equations