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.

Equations

• CategoryTheory.Bicategory.Comonad t = Comon_Class t

@[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.

Equations

• CategoryTheory.Bicategory.Comonad.counit = Comon_Class.counit

@[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.

Equations

• CategoryTheory.Bicategory.Comonad.comul = Comon_Class.comul

def CategoryTheory.Bicategory.termε : Lean.ParserDescr

The counit 2-morphism of the comonad.

Equations

• CategoryTheory.Bicategory.termε = Lean.ParserDescr.node `CategoryTheory.Bicategory.termε 1024 (Lean.ParserDescr.symbol "ε")

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

The counit 2-morphism of the comonad.

Equations

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

def CategoryTheory.Bicategory.termΔ : Lean.ParserDescr

The comultiplication 2-morphism of the comonad.

Equations

• CategoryTheory.Bicategory.termΔ = Lean.ParserDescr.node `CategoryTheory.Bicategory.termΔ 1024 (Lean.ParserDescr.symbol "Δ")

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

The comultiplication 2-morphism of the comonad.

Equations

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

@[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)

Equations

• CategoryTheory.Bicategory.Comonad.instId = inferInstanceAs (Comon_Class (CategoryTheory.MonoidalCategoryStruct.tensorUnit (a ⟶ 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.

Equations

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

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.

Equations

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

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

The bicategory of comonads in B.

Equations

• CategoryTheory.Bicategory.OplaxTrans.ComonadBicat B = CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete Unit)) B

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

The bicategory of comonads in B.

Equations

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

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.

Equations

• m.toOplax = m

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

The object in B associated with the comonad.

Equations

• m.obj = m.toOplax.obj { as := { as := PUnit.unit } }

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.

Equations

• m.hom = m.toOplax.map (CategoryTheory.CategoryStruct.id { as := { as := PUnit.unit } })

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

Equations

• m.instComonadHom = CategoryTheory.Bicategory.Comonad.ofOplaxFromUnit m.toOplax

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.

Equations

• CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad t = CategoryTheory.Bicategory.Comonad.toOplax t

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