Comonads in a bicategory

We define comonads in a bicategory B as comonoid objects in an endomorphism monoidal category. We show that this is equivalent to oplax functors from the trivial bicategory to B. From this, we show that comonads in B form a bicategory.

TODO

We can also define monads in a bicategory. This is not yet done as we don't have the bicategory structure on the set of lax functors at this point, which is needed to show that monads form a bicategory.

@[reducible, inline]

abbrev CategoryTheory.Bicategory.Comonad {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) : Type w

A comonad in a bicategory B is a 1-morphism t : a ⟶ a together with 2-morphisms Δ : t ⟶ t ≫ t and ε : t ⟶ 𝟙 a satisfying the comonad laws.

@[reducible, inline]

abbrev CategoryTheory.Bicategory.Comonad.counit {B : Type u} [Bicategory B] {a : B} {t : a ⟶ a} [Comonad t] : t ⟶ CategoryStruct.id a

The counit 2-morphism of the comonad.

@[reducible, inline]

abbrev CategoryTheory.Bicategory.Comonad.comul {B : Type u} [Bicategory B] {a : B} {t : a ⟶ a} [Comonad t] : t ⟶ CategoryStruct.comp t t

The comultiplication 2-morphism of the comonad.

def CategoryTheory.Bicategory.termε : Lean.ParserDescr

The counit 2-morphism of the comonad.

def CategoryTheory.Bicategory.«termε[_]» : Lean.ParserDescr

The counit 2-morphism of the comonad.

def CategoryTheory.Bicategory.termΔ : Lean.ParserDescr

The comultiplication 2-morphism of the comonad.

def CategoryTheory.Bicategory.«termΔ[_]» : Lean.ParserDescr

The comultiplication 2-morphism of the comonad.

@[simp]

theorem CategoryTheory.Bicategory.Comonad.counit_comul {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : CategoryStruct.comp comul (whiskerRight counit t) = (leftUnitor t).inv

@[simp]

theorem CategoryTheory.Bicategory.Comonad.counit_comul_assoc {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] {Z : a ⟶ a} (h : CategoryStruct.comp (CategoryStruct.id a) t ⟶ Z) : CategoryStruct.comp comul (CategoryStruct.comp (whiskerRight counit t) h) = CategoryStruct.comp (leftUnitor t).inv h

@[simp]

theorem CategoryTheory.Bicategory.Comonad.comul_counit {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : CategoryStruct.comp comul (whiskerLeft t counit) = (rightUnitor t).inv

@[simp]

theorem CategoryTheory.Bicategory.Comonad.comul_counit_assoc {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] {Z : a ⟶ a} (h : CategoryStruct.comp t (CategoryStruct.id a) ⟶ Z) : CategoryStruct.comp comul (CategoryStruct.comp (whiskerLeft t counit) h) = CategoryStruct.comp (rightUnitor t).inv h

@[simp]

theorem CategoryTheory.Bicategory.Comonad.comul_assoc {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : CategoryStruct.comp comul (whiskerLeft t comul) = CategoryStruct.comp comul (CategoryStruct.comp (whiskerRight comul t) (associator t t t).hom)

@[simp]

theorem CategoryTheory.Bicategory.Comonad.comul_assoc_assoc {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] {Z : a ⟶ a} (h : CategoryStruct.comp t (CategoryStruct.comp t t) ⟶ Z) : CategoryStruct.comp comul (CategoryStruct.comp (whiskerLeft t comul) h) = CategoryStruct.comp comul (CategoryStruct.comp (whiskerRight comul t) (CategoryStruct.comp (associator t t t).hom h))

theorem CategoryTheory.Bicategory.Comonad.comul_assoc_flip {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : CategoryStruct.comp comul (whiskerRight comul t) = CategoryStruct.comp comul (CategoryStruct.comp (whiskerLeft t comul) (associator t t t).inv)

theorem CategoryTheory.Bicategory.Comonad.comul_assoc_flip_assoc {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] {Z : a ⟶ a} (h : CategoryStruct.comp (CategoryStruct.comp t t) t ⟶ Z) : CategoryStruct.comp comul (CategoryStruct.comp (whiskerRight comul t) h) = CategoryStruct.comp comul (CategoryStruct.comp (whiskerLeft t comul) (CategoryStruct.comp (associator t t t).inv h))

instance CategoryTheory.Bicategory.Comonad.instId {B : Type u} [Bicategory B] {a : B} : Comonad (CategoryStruct.id a)

@[simp]

theorem CategoryTheory.Bicategory.Comonad.counit_def {B : Type u} [Bicategory B] {a : B} : Comon_Class.counit = CategoryStruct.id (CategoryStruct.id a)

def CategoryTheory.Bicategory.Comonad.ofOplaxFromUnit {B : Type u} [Bicategory B] (F : OplaxFunctor (LocallyDiscrete (Discrete Unit)) B) : Comonad (F.map (CategoryStruct.id { as := { as := () } }))

An oplax functor from the trivial bicategory to B defines a comonad in B.

def CategoryTheory.Bicategory.Comonad.toOplax {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : OplaxFunctor (LocallyDiscrete (Discrete Unit)) B

A comonad in B defines an oplax functor from the trivial bicategory to B.

def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat (B : Type u) [Bicategory B] : Type (max (max (max u v) 0) w)

The bicategory of comonads in B.

def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.inst {B : Type u} [Bicategory B] : Bicategory (ComonadBicat B)

The bicategory of comonads in B.

def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.toOplax {B : Type u} [Bicategory B] (m : ComonadBicat B) : OplaxFunctor (LocallyDiscrete (Discrete PUnit.{1})) B

The oplax functor from the trivial bicategory to B associated with the comonad.

def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.obj {B : Type u} [Bicategory B] (m : ComonadBicat B) : B

The object in B associated with the comonad.

def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.hom {B : Type u} [Bicategory B] (m : ComonadBicat B) : m.obj ⟶ m.obj

The morphism in B associated with the comonad.

instance CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.instComonadHom {B : Type u} [Bicategory B] (m : ComonadBicat B) : Comonad m.hom

def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : ComonadBicat B

Construct a comonad as an object in ComonadBicat B.

theorem CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_hom {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : (mkOfComonad t).hom = t

theorem CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_counit {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : Comonad.counit = Comonad.counit

theorem CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_comul {B : Type u} [Bicategory B] {a : B} (t : a ⟶ a) [Comonad t] : Comonad.comul = Comonad.comul