mathlib documentation

category_theory.monad.bundled

Bundled Monads

We define bundled (co)monads as a structure consisting of a functor func : C ⥤ C endowed with a term of type (co)monad func. See category_theory.monad.basic for the definition. The type of bundled (co)monads on a category C is denoted (Co)Monad C.

We also define morphisms of bundled (co)monads as morphisms of their underlying (co)monads in the sense of category_theory.(co)monad_hom. We construct a category instance on (Co)Monad C.

structure category_theory.Monad (C : Type u) [category_theory.category C] :

Type (max u v)

func : C ⥤ C
str : category_theory.monad c.func . "apply_instance"

Bundled monads.

structure category_theory.Comonad (C : Type u) [category_theory.category C] :

Type (max u v)

func : C ⥤ C
str : category_theory.comonad c.func . "apply_instance"

Bundled comonads

def category_theory.Monad.initial (C : Type u) [category_theory.category C] :

category_theory.Monad C

The initial monad. TODO: Prove it's initial.

Equations

category_theory.Monad.initial C = {func := 𝟭 C _inst_1, str := category_theory.monad.category_theory.monad _inst_1}

@[instance]

def category_theory.Monad.inhabited {C : Type u} [category_theory.category C] :

inhabited (category_theory.Monad C)

Equations

category_theory.Monad.inhabited = {default := category_theory.Monad.initial C _inst_1}

@[instance]

def category_theory.Monad.category_theory.monad {C : Type u} [category_theory.category C] {M : category_theory.Monad C} :

category_theory.monad M.func

Equations

category_theory.Monad.category_theory.monad = M.str

def category_theory.Monad.hom {C : Type u} [category_theory.category C] (M N : category_theory.Monad C) :

Type (max u v)

Morphisms of bundled monads.

Equations

M.hom N = category_theory.monad_hom M.func N.func

@[instance]

def category_theory.Monad.hom.inhabited {C : Type u} [category_theory.category C] {M : category_theory.Monad C} :

inhabited (M.hom M)

Equations

category_theory.Monad.hom.inhabited = {default := category_theory.monad_hom.id M.func category_theory.Monad.category_theory.monad}

@[instance]

def category_theory.Monad.category_theory.category {C : Type u} [category_theory.category C] :

category_theory.category (category_theory.Monad C)

Equations

category_theory.Monad.category_theory.category = {to_category_struct := {to_has_hom := {hom := category_theory.Monad.hom _inst_1}, id := λ (_x : category_theory.Monad C), category_theory.monad_hom.id _x.func, comp := λ (_x _x_1 _x_2 : category_theory.Monad C), category_theory.monad_hom.comp}, id_comp' := _, comp_id' := _, assoc' := _}

def category_theory.Monad.forget (C : Type u) [category_theory.category C] :

category_theory.Monad C ⥤ C ⥤ C

The forgetful functor from Monad C to C ⥤ C.

Equations

category_theory.Monad.forget C = {obj := category_theory.Monad.func _inst_1, map := λ (_x _x_1 : category_theory.Monad C) (f : _x ⟶ _x_1), f.to_nat_trans, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.Monad.comp_to_nat_trans {C : Type u} [category_theory.category C] {M N L : category_theory.Monad C} (f : M ⟶ N) (g : N ⟶ L) :

(f ≫ g).to_nat_trans = f.to_nat_trans.vcomp g.to_nat_trans

@[simp]

theorem category_theory.Monad.assoc_func_app {C : Type u} [category_theory.category C] {M : category_theory.Monad C} {X : C} :

M.func.map ((μ_ M.func).app X) ≫ (μ_ M.func).app X = (μ_ M.func).app (M.func.obj X) ≫ (μ_ M.func).app X

def category_theory.Comonad.terminal (C : Type u) [category_theory.category C] :

category_theory.Comonad C

The terminal comonad. TODO: Prove it's terminal.

Equations

category_theory.Comonad.terminal C = {func := 𝟭 C _inst_1, str := category_theory.comonad.category_theory.comonad _inst_1}

@[instance]

def category_theory.Comonad.inhabited {C : Type u} [category_theory.category C] :

inhabited (category_theory.Comonad C)

Equations

category_theory.Comonad.inhabited = {default := category_theory.Comonad.terminal C _inst_1}

@[instance]

def category_theory.Comonad.category_theory.comonad {C : Type u} [category_theory.category C] {M : category_theory.Comonad C} :

category_theory.comonad M.func

Equations

category_theory.Comonad.category_theory.comonad = M.str

def category_theory.Comonad.hom {C : Type u} [category_theory.category C] (M N : category_theory.Comonad C) :

Type (max u v)

Morphisms of bundled comonads.

Equations

M.hom N = category_theory.comonad_hom M.func N.func

@[instance]

def category_theory.Comonad.hom.inhabited {C : Type u} [category_theory.category C] {M : category_theory.Comonad C} :

inhabited (M.hom M)

Equations

category_theory.Comonad.hom.inhabited = {default := category_theory.comonad_hom.id M.func category_theory.Comonad.category_theory.comonad}

@[instance]

def category_theory.Comonad.category_theory.category {C : Type u} [category_theory.category C] :

category_theory.category (category_theory.Comonad C)

Equations

category_theory.Comonad.category_theory.category = {to_category_struct := {to_has_hom := {hom := category_theory.Comonad.hom _inst_1}, id := λ (_x : category_theory.Comonad C), category_theory.comonad_hom.id _x.func, comp := λ (_x _x_1 _x_2 : category_theory.Comonad C), category_theory.comonad_hom.comp}, id_comp' := _, comp_id' := _, assoc' := _}

def category_theory.Comonad.forget (C : Type u) [category_theory.category C] :

category_theory.Comonad C ⥤ C ⥤ C

The forgetful functor from CoMonad C to C ⥤ C.

Equations

category_theory.Comonad.forget C = {obj := category_theory.Comonad.func _inst_1, map := λ (_x _x_1 : category_theory.Comonad C) (f : _x ⟶ _x_1), f.to_nat_trans, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.Comonad.comp_to_nat_trans {C : Type u} [category_theory.category C] {M N L : category_theory.Comonad C} (f : M ⟶ N) (g : N ⟶ L) :

(f ≫ g).to_nat_trans = f.to_nat_trans.vcomp g.to_nat_trans

@[simp]

theorem category_theory.Comonad.coassoc_func_app {C : Type u} [category_theory.category C] {M : category_theory.Comonad C} {X : C} :

(δ_ M.func).app X ≫ M.func.map ((δ_ M.func).app X) = (δ_ M.func).app X ≫ (δ_ M.func).app (M.func.obj X)