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

This file has been adapted to Mathlib.CategoryTheory.Monad.Equalizer. Please try to keep them in sync.

Show that any algebra is a coequalizer of free algebras.

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

The top map in the coequalizer diagram we will construct.

Equations

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

@[simp]

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

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

The bottom map in the coequalizer diagram we will construct.

Equations

• CategoryTheory.Monad.FreeCoequalizer.bottomMap X = { f := T.μ.app X.A, h := ⋯ }

@[simp]

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

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

The cofork map in the coequalizer diagram we will construct.

Equations

• CategoryTheory.Monad.FreeCoequalizer.π X = { f := X.a, h := ⋯ }

@[simp]

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

theorem CategoryTheory.Monad.FreeCoequalizer.condition {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : 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.instIsReflexivePairAlgebraTopMapBottomMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : CategoryTheory.IsReflexivePair (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.bottomMap X)

Equations

• ⋯ = ⋯

def CategoryTheory.Monad.beckAlgebraCofork {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : 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

• CategoryTheory.Monad.beckAlgebraCofork X = CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Monad.FreeCoequalizer.π X) ⋯

@[simp]

theorem CategoryTheory.Monad.beckAlgebraCofork_ι_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) (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 : T.Algebra) : (CategoryTheory.Monad.beckAlgebraCofork X).pt = X

def CategoryTheory.Monad.beckAlgebraCoequalizer {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : 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 : T.Algebra) : CategoryTheory.IsSplitCoequalizer (T.map X.a) (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.

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

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

Equations

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

@[simp]

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

@[simp]

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

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

The Beck cofork is a coequalizer.

Equations

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

@[simp]

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