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.lean. 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₁} [Category.{v₁, u₁} C] {T : 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.

@[simp]

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

def CategoryTheory.Monad.FreeCoequalizer.bottomMap {C : Type u₁} [Category.{v₁, u₁} C] {T : 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.

@[simp]

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

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

The cofork map in the coequalizer diagram we will construct.

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

The Beck cofork is a split coequalizer.

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

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

@[simp]

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

@[simp]

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

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

The Beck cofork is a coequalizer.

@[simp]

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