- to_functor : C ⥤ C
- η' : 𝟭 C ⟶ c.to_functor
- μ' : c.to_functor ⋙ c.to_functor ⟶ c.to_functor
- assoc' : (∀ (X : C), c.to_functor.map (c.μ'.app X) ≫ c.μ'.app X = c.μ'.app (c.to_functor.obj X) ≫ c.μ'.app X) . "obviously"
- left_unit' : (∀ (X : C), c.η'.app (c.to_functor.obj X) ≫ c.μ'.app X = 𝟙 ((𝟭 C).obj (c.to_functor.obj X))) . "obviously"
- right_unit' : (∀ (X : C), c.to_functor.map (c.η'.app X) ≫ c.μ'.app X = 𝟙 (c.to_functor.obj ((𝟭 C).obj X))) . "obviously"
The data of a monad on C consists of an endofunctor T together with natural transformations η : 𝟭 C ⟶ T and μ : T ⋙ T ⟶ T satisfying three equations:
- T μ_X ≫ μ_X = μ_(TX) ≫ μ_X (associativity)
- η_(TX) ≫ μ_X = 1_X (left unit)
- Tη_X ≫ μ_X = 1_X (right unit)
- to_functor : C ⥤ C
- ε' : c.to_functor ⟶ 𝟭 C
- δ' : c.to_functor ⟶ c.to_functor ⋙ c.to_functor
- coassoc' : (∀ (X : C), c.δ'.app X ≫ c.to_functor.map (c.δ'.app X) = c.δ'.app X ≫ c.δ'.app (c.to_functor.obj X)) . "obviously"
- left_counit' : (∀ (X : C), c.δ'.app X ≫ c.ε'.app (c.to_functor.obj X) = 𝟙 (c.to_functor.obj X)) . "obviously"
- right_counit' : (∀ (X : C), c.δ'.app X ≫ c.to_functor.map (c.ε'.app X) = 𝟙 (c.to_functor.obj X)) . "obviously"
The data of a comonad on C consists of an endofunctor G together with natural transformations ε : G ⟶ 𝟭 C and δ : G ⟶ G ⋙ G satisfying three equations:
- δ_X ≫ G δ_X = δ_X ≫ δ_(GX) (coassociativity)
- δ_X ≫ ε_(GX) = 1_X (left counit)
- δ_X ≫ G ε_X = 1_X (right counit)
Equations
- category_theory.coe_monad = {coe := λ (T : category_theory.monad C), T.to_functor}
Equations
- category_theory.coe_comonad = {coe := λ (G : category_theory.comonad C), G.to_functor}
The unit for the monad T
.
The multiplication for the monad T
.
The counit for the comonad G
.
The comultiplication for the comonad G
.
A custom simps projection for the functor part of a monad, as a coercion.
Equations
A custom simps projection for the unit of a monad, in simp normal form.
Equations
A custom simps projection for the multiplication of a monad, in simp normal form.
Equations
A custom simps projection for the functor part of a comonad, as a coercion.
Equations
A custom simps projection for the counit of a comonad, in simp normal form.
Equations
A custom simps projection for the comultiplication of a comonad, in simp normal form.
Equations
- to_nat_trans : category_theory.nat_trans ↑T₁ ↑T₂
- app_η' : (∀ {X : C}, T₁.η.app X ≫ c.to_nat_trans.app X = T₂.η.app X) . "obviously"
- app_μ' : (∀ {X : C}, T₁.μ.app X ≫ c.to_nat_trans.app X = (↑T₁.map (c.to_nat_trans.app X) ≫ c.to_nat_trans.app (↑T₂.obj X)) ≫ T₂.μ.app X) . "obviously"
A morphism of monads is a natural transformation compatible with η and μ.
- to_nat_trans : category_theory.nat_trans ↑M ↑N
- app_ε' : (∀ {X : C}, c.to_nat_trans.app X ≫ N.ε.app X = M.ε.app X) . "obviously"
- app_δ' : (∀ {X : C}, c.to_nat_trans.app X ≫ N.δ.app X = M.δ.app X ≫ c.to_nat_trans.app (M.to_functor.obj X) ≫ N.to_functor.map (c.to_nat_trans.app X)) . "obviously"
A morphism of comonads is a natural transformation compatible with ε and δ.
Equations
- category_theory.monad.category = {to_category_struct := {to_has_hom := {hom := category_theory.monad_hom _inst_1}, id := λ (M : category_theory.monad C), {to_nat_trans := 𝟙 ↑M, app_η' := _, app_μ' := _}, comp := λ (_x _x_1 _x_2 : category_theory.monad C) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), {to_nat_trans := {app := λ (X : C), f.to_nat_trans.app X ≫ g.to_nat_trans.app X, naturality' := _}, app_η' := _, app_μ' := _}}, id_comp' := _, comp_id' := _, assoc' := _}
Equations
- category_theory.comonad.category = {to_category_struct := {to_has_hom := {hom := category_theory.comonad_hom _inst_1}, id := λ (M : category_theory.comonad C), {to_nat_trans := 𝟙 ↑M, app_ε' := _, app_δ' := _}, comp := λ (M N L : category_theory.comonad C) (f : M ⟶ N) (g : N ⟶ L), {to_nat_trans := {app := λ (X : C), f.to_nat_trans.app X ≫ g.to_nat_trans.app X, naturality' := _}, app_ε' := _, app_δ' := _}}, id_comp' := _, comp_id' := _, assoc' := _}
Equations
Equations
The forgetful functor from the category of monads to the category of endofunctors.
Equations
- category_theory.monad_to_functor C = {obj := λ (T : category_theory.monad C), ↑T, map := λ (M N : category_theory.monad C) (f : M ⟶ N), f.to_nat_trans, map_id' := _, map_comp' := _}
The forgetful functor from the category of comonads to the category of endofunctors.
Equations
- category_theory.comonad_to_functor C = {obj := λ (G : category_theory.comonad C), ↑G, map := λ (M N : category_theory.comonad C) (f : M ⟶ N), f.to_nat_trans, map_id' := _, map_comp' := _}
An isomorphism of monads gives a natural isomorphism of the underlying functors.
Equations
An isomorphism of comonads gives a natural isomorphism of the underlying functors.
Equations
The identity monad.
Equations
- category_theory.monad.id C = {to_functor := 𝟭 C _inst_1, η' := 𝟙 (𝟭 C), μ' := 𝟙 (𝟭 C), assoc' := _, left_unit' := _, right_unit' := _}
Equations
- category_theory.monad.inhabited C = {default := category_theory.monad.id C _inst_1}
The identity comonad.
Equations
- category_theory.comonad.id C = {to_functor := 𝟭 C _inst_1, ε' := 𝟙 (𝟭 C), δ' := 𝟙 (𝟭 C), coassoc' := _, left_counit' := _, right_counit' := _}
Equations
- category_theory.comonad.inhabited C = {default := category_theory.comonad.id C _inst_1}