Special equalizers associated to a comonad

Associated to a comonad T : C ⥤ C we have important equalizer constructions: Any coalgebra is an equalizer (in the category of coalgebras) of cofree coalgebras. Furthermore, this equalizer is coreflexive. In C, this fork diagram is a split equalizer (in particular, it is still an equalizer). This split equalizer is known as the Beck equalizer (as it features heavily in Beck's comonadicity theorem).

This file is adapted from Mathlib/CategoryTheory/Monad/Coequalizer.lean. Please try to keep them in sync.

Show that any coalgebra is an equalizer of cofree coalgebras.

def CategoryTheory.Comonad.CofreeEqualizer.topMap {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : T.cofree.obj X.A ⟶ T.cofree.obj (T.obj X.A)

The top map in the equalizer diagram we will construct.

@[simp]

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

def CategoryTheory.Comonad.CofreeEqualizer.bottomMap {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : T.cofree.obj X.A ⟶ T.cofree.obj (T.obj X.A)

The bottom map in the equalizer diagram we will construct.

@[simp]

theorem CategoryTheory.Comonad.CofreeEqualizer.bottomMap_f {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : (bottomMap X).f = T.δ.app X.A

def CategoryTheory.Comonad.CofreeEqualizer.ι {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : X ⟶ T.cofree.obj X.A

The fork map in the equalizer diagram we will construct.

@[simp]

theorem CategoryTheory.Comonad.CofreeEqualizer.ι_f {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : (ι X).f = X.a

theorem CategoryTheory.Comonad.CofreeEqualizer.condition {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : CategoryStruct.comp (ι X) (topMap X) = CategoryStruct.comp (ι X) (bottomMap X)

instance CategoryTheory.Comonad.instIsCoreflexivePairCoalgebraTopMapBottomMap {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)

def CategoryTheory.Comonad.beckCoalgebraFork {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : Limits.Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)

Construct the Beck fork in the category of coalgebras. This fork is coreflexive as well as an equalizer.

@[simp]

theorem CategoryTheory.Comonad.beckCoalgebraFork_π_app {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) (X✝ : Limits.WalkingParallelPair) : (beckCoalgebraFork X).π.app X✝ = Limits.WalkingParallelPair.rec (motive := fun (t : Limits.WalkingParallelPair) => X✝ = t → (X ⟶ (Limits.parallelPair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)).obj X✝)) (fun (h : X✝ = Limits.WalkingParallelPair.zero) => ⋯ ▸ CofreeEqualizer.ι X) (fun (h : X✝ = Limits.WalkingParallelPair.one) => ⋯ ▸ CategoryStruct.comp (CofreeEqualizer.ι X) (CofreeEqualizer.topMap X)) X✝ ⋯

@[simp]

theorem CategoryTheory.Comonad.beckCoalgebraFork_pt {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : (beckCoalgebraFork X).pt = X

def CategoryTheory.Comonad.beckCoalgebraEqualizer {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : Limits.IsLimit (beckCoalgebraFork X)

The fork constructed is a limit. This shows that any coalgebra is a (coreflexive) equalizer of cofree coalgebras.

def CategoryTheory.Comonad.beckSplitEqualizer {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : IsSplitEqualizer (T.map X.a) (T.δ.app X.A) X.a

The Beck fork is a split equalizer.

def CategoryTheory.Comonad.beckFork {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : Limits.Fork (T.map X.a) (T.δ.app X.A)

This is the Beck fork. It is a split equalizer, in particular a equalizer.

@[simp]

theorem CategoryTheory.Comonad.beckFork_pt {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : (beckFork X).pt = X.A

@[simp]

theorem CategoryTheory.Comonad.beckFork_ι {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : (beckFork X).ι = X.a

def CategoryTheory.Comonad.beckEqualizer {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) : Limits.IsLimit (beckFork X)

The Beck fork is a equalizer.

@[simp]

theorem CategoryTheory.Comonad.beckEqualizer_lift {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} (X : T.Coalgebra) (s : Limits.Fork (T.map X.a) (T.δ.app X.A)) : (beckEqualizer X).lift s = CategoryStruct.comp s.ι (T.ε.app X.A)