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.
- func : C ⥤ C
- str : category_theory.monad c.func . "apply_instance"
Bundled monads.
- func : C ⥤ C
- str : category_theory.comonad c.func . "apply_instance"
Bundled comonads
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]
Equations
@[instance]
def
category_theory.Monad.category_theory.monad
{C : Type u}
[category_theory.category C]
{M : category_theory.Monad C} :
Equations
def
category_theory.Monad.hom
{C : Type u}
[category_theory.category C] :
category_theory.Monad C → 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} :
@[instance]
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 = {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
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]
Equations
@[instance]
def
category_theory.Comonad.category_theory.comonad
{C : Type u}
[category_theory.category C]
{M : category_theory.Comonad C} :
Equations
def
category_theory.Comonad.hom
{C : Type u}
[category_theory.category C] :
category_theory.Comonad C → 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} :
@[instance]
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 = {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