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₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.FreeCoequalizer.topMap X).f = T.toPrefunctor.map X.a

def CategoryTheory.Monad.FreeCoequalizer.topMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.free T).toPrefunctor.obj (T.toPrefunctor.obj X.A) ⟶ (CategoryTheory.Monad.free T).toPrefunctor.obj X.A

The top map in the coequalizer diagram we will construct.

Equations

• CategoryTheory.Monad.FreeCoequalizer.topMap X = (CategoryTheory.Monad.free T).toPrefunctor.map X.a

@[simp]

theorem CategoryTheory.Monad.FreeCoequalizer.bottomMap_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.FreeCoequalizer.bottomMap X).f = (CategoryTheory.Monad.μ T).app X.A

def CategoryTheory.Monad.FreeCoequalizer.bottomMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.free T).toPrefunctor.obj (T.toPrefunctor.obj X.A) ⟶ (CategoryTheory.Monad.free T).toPrefunctor.obj X.A

The bottom map in the coequalizer diagram we will construct.

Equations

• CategoryTheory.Monad.FreeCoequalizer.bottomMap X = CategoryTheory.Monad.Algebra.Hom.mk ((CategoryTheory.Monad.μ T).app X.A)

@[simp]

theorem CategoryTheory.Monad.FreeCoequalizer.π_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.FreeCoequalizer.π X).f = X.a

def CategoryTheory.Monad.FreeCoequalizer.π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.free T).toPrefunctor.obj X.A ⟶ X

The cofork map in the coequalizer diagram we will construct.

Equations

• CategoryTheory.Monad.FreeCoequalizer.π X = CategoryTheory.Monad.Algebra.Hom.mk X.a

theorem CategoryTheory.Monad.FreeCoequalizer.condition {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.π X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.bottomMap X) (CategoryTheory.Monad.FreeCoequalizer.π X)

instance CategoryTheory.Monad.instIsReflexivePairAlgebraEilenbergMooreObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorFreeObjToPrefunctorToFunctorATopMapBottomMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : CategoryTheory.IsReflexivePair (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.bottomMap X)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Monad.beckAlgebraCofork_ι_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) (X : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Monad.beckAlgebraCofork X✝).ι.app X = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.topMap X✝) (CategoryTheory.Monad.FreeCoequalizer.π X✝)) (CategoryTheory.Monad.FreeCoequalizer.π X✝) X

@[simp]

theorem CategoryTheory.Monad.beckAlgebraCofork_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.beckAlgebraCofork X).pt = X

def CategoryTheory.Monad.beckAlgebraCofork {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : CategoryTheory.Limits.Cofork (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.bottomMap X)

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Monad.beckAlgebraCoequalizer {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.beckAlgebraCofork X)

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Monad.beckSplitCoequalizer {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : CategoryTheory.IsSplitCoequalizer (T.toPrefunctor.map X.a) ((CategoryTheory.Monad.μ T).app X.A) X.a

The Beck cofork is a split coequalizer.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Monad.beckCofork_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.beckCofork X).pt = X.A

def CategoryTheory.Monad.beckCofork {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : CategoryTheory.Limits.Cofork (T.toPrefunctor.map X.a) ((CategoryTheory.Monad.μ T).app X.A)

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

Equations

• CategoryTheory.Monad.beckCofork X = CategoryTheory.IsSplitCoequalizer.asCofork (CategoryTheory.Monad.beckSplitCoequalizer X)

@[simp]

theorem CategoryTheory.Monad.beckCofork_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : CategoryTheory.Limits.Cofork.π (CategoryTheory.Monad.beckCofork X) = X.a

def CategoryTheory.Monad.beckCoequalizer {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.beckCofork X)

The Beck cofork is a coequalizer.

Equations

• CategoryTheory.Monad.beckCoequalizer X = CategoryTheory.IsSplitCoequalizer.isCoequalizer (CategoryTheory.Monad.beckSplitCoequalizer X)

@[simp]

theorem CategoryTheory.Monad.beckCoequalizer_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) (s : CategoryTheory.Limits.Cofork (T.toPrefunctor.map X.a) ((CategoryTheory.Monad.μ T).app X.A)) : (CategoryTheory.Monad.beckCoequalizer X).desc s = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T).app X.A) (CategoryTheory.Limits.Cofork.π s)