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)

Bundled monads.

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

Bundled comonads

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

Equations

Morphisms of bundled monads.

Equations

The forgetful functor from Monad C to C ⥤ C.

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

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

Equations

Morphisms of bundled comonads.

Equations

The forgetful functor from CoMonad C to C ⥤ C.

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