Documentation

Mathlib.CategoryTheory.Bicategory.Monad.Basic

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

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.

Instances For

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

Instances For

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

Instances For

def CategoryTheory.Bicategory.termε :

Lean.ParserDescr

The counit 2-morphism of the comonad.

Instances For

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

Lean.ParserDescr

The counit 2-morphism of the comonad.

Instances For

def CategoryTheory.Bicategory.termΔ :

Lean.ParserDescr

The comultiplication 2-morphism of the comonad.

Instances For

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

Lean.ParserDescr

The comultiplication 2-morphism of the comonad.

Instances For

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

@[implicit_reducible]

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} :

ComonObj.counit = CategoryStruct.id (CategoryStruct.id a)

@[implicit_reducible]

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.

Instances For

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.

Instances For

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

Type (max (max (max u v) 0) w)

The bicategory of comonads in B.

Instances For

@[implicit_reducible]

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

Bicategory (ComonadBicat B)

The bicategory of comonads in B.

Instances For

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.

Instances For

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

B

The object in B associated with the comonad.

Instances For

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.

Instances For

@[implicit_reducible]

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

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

Construct a comonad as an object in ComonadBicat B.

Instances For

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