Monads

We construct the categories of monads and comonads, and their forgetful functors to endofunctors.

(Note that these are the category theorist's monads, not the programmers monads. For the translation, see the file CategoryTheory.Monad.Types.)

For the fact that monads are "just" monoids in the category of endofunctors, see the file CategoryTheory.Monad.EquivMon.

structure CategoryTheory.Monad (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] extends CategoryTheory.Functor : Type (max u₁ v₁)

• obj : C → C
• map : {X Y : C} → (X ⟶ Y) → (s.obj X ⟶ s.obj Y)
• map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
• map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
• η' : CategoryTheory.Functor.id C ⟶ s.toFunctor
• μ' : CategoryTheory.Functor.comp s.toFunctor s.toFunctor ⟶ s.toFunctor
• assoc' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.map (s.μ'.app X)) (s.μ'.app X) = CategoryTheory.CategoryStruct.comp (s.μ'.app (s.obj X)) (s.μ'.app X)
• left_unit' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.η'.app (s.obj X)) (s.μ'.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (s.obj X))
• right_unit' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.map (s.η'.app X)) (s.μ'.app X) = CategoryTheory.CategoryStruct.id (s.obj ((CategoryTheory.Functor.id C).obj X))

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)

structure CategoryTheory.Comonad (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] extends CategoryTheory.Functor : Type (max u₁ v₁)

• obj : C → C
• map : {X Y : C} → (X ⟶ Y) → (s.obj X ⟶ s.obj Y)
• map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
• map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
• ε' : s.toFunctor ⟶ CategoryTheory.Functor.id C
• δ' : s.toFunctor ⟶ CategoryTheory.Functor.comp s.toFunctor s.toFunctor
• coassoc' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.δ'.app X) (s.map (s.δ'.app X)) = CategoryTheory.CategoryStruct.comp (s.δ'.app X) (s.δ'.app (s.obj X))
• left_counit' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.δ'.app X) (s.ε'.app (s.obj X)) = CategoryTheory.CategoryStruct.id (s.obj X)
• right_counit' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.δ'.app X) (s.map (s.ε'.app X)) = CategoryTheory.CategoryStruct.id (s.obj X)

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)

instance CategoryTheory.coeMonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : Coe (CategoryTheory.Monad C) (CategoryTheory.Functor C C)

instance CategoryTheory.coeComonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : Coe (CategoryTheory.Comonad C) (CategoryTheory.Functor C C)

def CategoryTheory.Monad.η {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor.id C ⟶ T.toFunctor

The unit for the monad T.

def CategoryTheory.Monad.μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor.comp T.toFunctor T.toFunctor ⟶ T.toFunctor

The multiplication for the monad T.

def CategoryTheory.Comonad.ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.toFunctor ⟶ CategoryTheory.Functor.id C

The counit for the comonad G.

def CategoryTheory.Comonad.δ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.toFunctor ⟶ CategoryTheory.Functor.comp G.toFunctor G.toFunctor

The comultiplication for the comonad G.

def CategoryTheory.Monad.Simps.coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor C C

A custom simps projection for the functor part of a monad, as a coercion.

def CategoryTheory.Monad.Simps.η {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor.id C ⟶ T.toFunctor

A custom simps projection for the unit of a monad, in simp normal form.

def CategoryTheory.Monad.Simps.μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor.comp T.toFunctor T.toFunctor ⟶ T.toFunctor

A custom simps projection for the multiplication of a monad, in simp normal form.

def CategoryTheory.Comonad.Simps.coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.Functor C C

A custom simps projection for the functor part of a comonad, as a coercion.

def CategoryTheory.Comonad.Simps.ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.toFunctor ⟶ CategoryTheory.Functor.id C

A custom simps projection for the counit of a comonad, in simp normal form.

def CategoryTheory.Comonad.Simps.δ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.toFunctor ⟶ CategoryTheory.Functor.comp G.toFunctor G.toFunctor

A custom simps projection for the comultiplication of a comonad, in simp normal form.

theorem CategoryTheory.Monad.assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) {Z : C} (h : T.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.map ((CategoryTheory.Monad.μ T).app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T).app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T).app (T.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T).app X) h)

theorem CategoryTheory.Monad.assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : CategoryTheory.CategoryStruct.comp (T.map ((CategoryTheory.Monad.μ T).app X)) ((CategoryTheory.Monad.μ T).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T).app (T.obj X)) ((CategoryTheory.Monad.μ T).app X)

@[simp]

theorem CategoryTheory.Monad.left_unit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) {Z : C} (h : T.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T).app (T.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T).app X) h) = h

@[simp]

theorem CategoryTheory.Monad.left_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T).app (T.obj X)) ((CategoryTheory.Monad.μ T).app X) = CategoryTheory.CategoryStruct.id (T.obj X)

@[simp]

theorem CategoryTheory.Monad.right_unit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) {Z : C} (h : T.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.map ((CategoryTheory.Monad.η T).app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T).app X) h) = h

@[simp]

theorem CategoryTheory.Monad.right_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : CategoryTheory.CategoryStruct.comp (T.map ((CategoryTheory.Monad.η T).app X)) ((CategoryTheory.Monad.μ T).app X) = CategoryTheory.CategoryStruct.id (T.obj X)

@[simp]

theorem CategoryTheory.Comonad.coassoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) {Z : C} (h : G.obj ((CategoryTheory.Functor.comp G.toFunctor G.toFunctor).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app X) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Comonad.δ G).app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app (G.obj X)) h)

@[simp]

theorem CategoryTheory.Comonad.coassoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app X) (G.map ((CategoryTheory.Comonad.δ G).app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app X) ((CategoryTheory.Comonad.δ G).app (G.obj X))

@[simp]

theorem CategoryTheory.Comonad.left_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) {Z : C} (h : (CategoryTheory.Functor.id C).obj (G.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.ε G).app (G.obj X)) h) = h

@[simp]

theorem CategoryTheory.Comonad.left_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app X) ((CategoryTheory.Comonad.ε G).app (G.obj X)) = CategoryTheory.CategoryStruct.id (G.obj X)

@[simp]

theorem CategoryTheory.Comonad.right_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) {Z : C} (h : G.obj ((CategoryTheory.Functor.id C).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app X) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Comonad.ε G).app X)) h) = h

@[simp]

theorem CategoryTheory.Comonad.right_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app X) (G.map ((CategoryTheory.Comonad.ε G).app X)) = CategoryTheory.CategoryStruct.id (G.obj X)

theorem CategoryTheory.MonadHom.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {T₁ T₂ : CategoryTheory.Monad C} (x y : CategoryTheory.MonadHom T₁ T₂), x = y ↔ x.app = y.app

theorem CategoryTheory.MonadHom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {T₁ T₂ : CategoryTheory.Monad C} (x y : CategoryTheory.MonadHom T₁ T₂), x.app = y.app → x = y

structure CategoryTheory.MonadHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T₁ : CategoryTheory.Monad C) (T₂ : CategoryTheory.Monad C) extends CategoryTheory.NatTrans : Type (max u₁ v₁)

• app : (X : C) → T₁.obj X ⟶ T₂.obj X
• naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (T₁.map f) (s.app Y) = CategoryTheory.CategoryStruct.comp (s.app X) (T₂.map f)
• app_η : ∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T₁).app X) (s.app X) = (CategoryTheory.Monad.η T₂).app X
• app_μ : ∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T₁).app X) (s.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (T₁.map (s.app X)) (s.app (T₂.obj X))) ((CategoryTheory.Monad.μ T₂).app X)

A morphism of monads is a natural transformation compatible with η and μ.

theorem CategoryTheory.ComonadHom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {M N : CategoryTheory.Comonad C} (x y : CategoryTheory.ComonadHom M N), x.app = y.app → x = y

theorem CategoryTheory.ComonadHom.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {M N : CategoryTheory.Comonad C} (x y : CategoryTheory.ComonadHom M N), x = y ↔ x.app = y.app

structure CategoryTheory.ComonadHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (M : CategoryTheory.Comonad C) (N : CategoryTheory.Comonad C) extends CategoryTheory.NatTrans : Type (max u₁ v₁)

• app : (X : C) → M.obj X ⟶ N.obj X
• naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (M.map f) (s.app Y) = CategoryTheory.CategoryStruct.comp (s.app X) (N.map f)
• app_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.app X) ((CategoryTheory.Comonad.ε N).app X) = (CategoryTheory.Comonad.ε M).app X
• app_δ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.app X) ((CategoryTheory.Comonad.δ N).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ M).app X) (CategoryTheory.CategoryStruct.comp (s.app (M.obj X)) (N.map (s.app X)))

A morphism of comonads is a natural transformation compatible with ε and δ.

@[simp]

theorem CategoryTheory.MonadHom.app_η_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (self : CategoryTheory.MonadHom T₁ T₂) (X : C) {Z : C} (h : T₂.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T₁).app X) (CategoryTheory.CategoryStruct.comp (self.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T₂).app X) h

@[simp]

theorem CategoryTheory.MonadHom.app_μ_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (self : CategoryTheory.MonadHom T₁ T₂) (X : C) {Z : C} (h : T₂.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T₁).app X) (CategoryTheory.CategoryStruct.comp (self.app X) h) = CategoryTheory.CategoryStruct.comp (T₁.map (self.app X)) (CategoryTheory.CategoryStruct.comp (self.app (T₂.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T₂).app X) h))

@[simp]

theorem CategoryTheory.ComonadHom.app_ε_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (self : CategoryTheory.ComonadHom M N) (X : C) {Z : C} (h : (CategoryTheory.Functor.id C).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.ε N).app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.ε M).app X) h

@[simp]

theorem CategoryTheory.ComonadHom.app_δ_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (self : CategoryTheory.ComonadHom M N) (X : C) {Z : C} (h : (CategoryTheory.Functor.comp N.toFunctor N.toFunctor).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ N).app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ M).app X) (CategoryTheory.CategoryStruct.comp (self.app (M.obj X)) (CategoryTheory.CategoryStruct.comp (N.map (self.app X)) h))

instance CategoryTheory.instQuiverMonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : Quiver (CategoryTheory.Monad C)

instance CategoryTheory.instQuiverComonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : Quiver (CategoryTheory.Comonad C)

theorem CategoryTheory.MonadHom.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂) (g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g

theorem CategoryTheory.ComonadHom.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Comonad C} {T₂ : CategoryTheory.Comonad C} (f : T₁ ⟶ T₂) (g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g

instance CategoryTheory.instCategoryMonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Category.{max u₁ v₁, max u₁ v₁} (CategoryTheory.Monad C)

instance CategoryTheory.instCategoryComonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Category.{max u₁ v₁, max u₁ v₁} (CategoryTheory.Comonad C)

instance CategoryTheory.instInhabitedMonadHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} : Inhabited (CategoryTheory.MonadHom T T)

@[simp]

theorem CategoryTheory.MonadHom.id_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : (CategoryTheory.CategoryStruct.id T).toNatTrans = CategoryTheory.CategoryStruct.id T.toFunctor

@[simp]

theorem CategoryTheory.MonadHom.comp_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} {T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) : (CategoryTheory.CategoryStruct.comp f g).toNatTrans = CategoryTheory.CategoryStruct.comp f.toNatTrans g.toNatTrans

instance CategoryTheory.instInhabitedComonadHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} : Inhabited (CategoryTheory.ComonadHom G G)

@[simp]

theorem CategoryTheory.ComonadHom.id_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C) : (CategoryTheory.CategoryStruct.id T).toNatTrans = CategoryTheory.CategoryStruct.id T.toFunctor

@[simp]

theorem CategoryTheory.comp_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Comonad C} {T₂ : CategoryTheory.Comonad C} {T₃ : CategoryTheory.Comonad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) : (CategoryTheory.CategoryStruct.comp f g).toNatTrans = CategoryTheory.CategoryStruct.comp f.toNatTrans g.toNatTrans

@[simp]

theorem CategoryTheory.MonadIso.mk_inv_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Monad C} {N : CategoryTheory.Monad C} (f : M.toFunctor ≅ N.toFunctor) (f_η : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η M).app X) (f.hom.app X) = (CategoryTheory.Monad.η N).app X) _auto✝) (f_μ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ M).app X) (f.hom.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) ((CategoryTheory.Monad.μ N).app X)) _auto✝) : (CategoryTheory.MonadIso.mk f).inv.toNatTrans = f.inv

@[simp]

theorem CategoryTheory.MonadIso.mk_hom_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Monad C} {N : CategoryTheory.Monad C} (f : M.toFunctor ≅ N.toFunctor) (f_η : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η M).app X) (f.hom.app X) = (CategoryTheory.Monad.η N).app X) _auto✝) (f_μ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ M).app X) (f.hom.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) ((CategoryTheory.Monad.μ N).app X)) _auto✝) : (CategoryTheory.MonadIso.mk f).hom.toNatTrans = f.hom

def CategoryTheory.MonadIso.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Monad C} {N : CategoryTheory.Monad C} (f : M.toFunctor ≅ N.toFunctor) (f_η : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η M).app X) (f.hom.app X) = (CategoryTheory.Monad.η N).app X) _auto✝) (f_μ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ M).app X) (f.hom.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) ((CategoryTheory.Monad.μ N).app X)) _auto✝) : M ≅ N

Construct a monad isomorphism from a natural isomorphism of functors where the forward direction is a monad morphism.

@[simp]

theorem CategoryTheory.ComonadIso.mk_hom_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (f : M.toFunctor ≅ N.toFunctor) (f_ε : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) ((CategoryTheory.Comonad.ε N).app X) = (CategoryTheory.Comonad.ε M).app X) _auto✝) (f_δ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) ((CategoryTheory.Comonad.δ N).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ M).app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))) _auto✝) : (CategoryTheory.ComonadIso.mk f).hom.toNatTrans = f.hom

@[simp]

theorem CategoryTheory.ComonadIso.mk_inv_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (f : M.toFunctor ≅ N.toFunctor) (f_ε : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) ((CategoryTheory.Comonad.ε N).app X) = (CategoryTheory.Comonad.ε M).app X) _auto✝) (f_δ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) ((CategoryTheory.Comonad.δ N).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ M).app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))) _auto✝) : (CategoryTheory.ComonadIso.mk f).inv.toNatTrans = f.inv

def CategoryTheory.ComonadIso.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (f : M.toFunctor ≅ N.toFunctor) (f_ε : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) ((CategoryTheory.Comonad.ε N).app X) = (CategoryTheory.Comonad.ε M).app X) _auto✝) (f_δ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) ((CategoryTheory.Comonad.δ N).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ M).app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))) _auto✝) : M ≅ N

Construct a comonad isomorphism from a natural isomorphism of functors where the forward direction is a comonad morphism.

@[simp]

theorem CategoryTheory.monadToFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : (CategoryTheory.monadToFunctor C).obj T = T.toFunctor

@[simp]

theorem CategoryTheory.monadToFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : CategoryTheory.Monad C} (f : X ⟶ Y), (CategoryTheory.monadToFunctor C).map f = f.toNatTrans

def CategoryTheory.monadToFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor (CategoryTheory.Monad C) (CategoryTheory.Functor C C)

The forgetful functor from the category of monads to the category of endofunctors.

instance CategoryTheory.instFaithfulMonadInstCategoryMonadFunctorCategoryMonadToFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Faithful (CategoryTheory.monadToFunctor C)

theorem CategoryTheory.monadToFunctor_mapIso_monad_iso_mk (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Monad C} {N : CategoryTheory.Monad C} (f : M.toFunctor ≅ N.toFunctor) (f_η : ∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η M).app X) (f.hom.app X) = (CategoryTheory.Monad.η N).app X) (f_μ : ∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ M).app X) (f.hom.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) ((CategoryTheory.Monad.μ N).app X)) : (CategoryTheory.monadToFunctor C).mapIso (CategoryTheory.MonadIso.mk f) = f

instance CategoryTheory.instReflectsIsomorphismsMonadInstCategoryMonadFunctorCategoryMonadToFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.monadToFunctor C)

@[simp]

theorem CategoryTheory.comonadToFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : CategoryTheory.Comonad C} (f : X ⟶ Y), (CategoryTheory.comonadToFunctor C).map f = f.toNatTrans

@[simp]

theorem CategoryTheory.comonadToFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : (CategoryTheory.comonadToFunctor C).obj G = G.toFunctor

def CategoryTheory.comonadToFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor (CategoryTheory.Comonad C) (CategoryTheory.Functor C C)

The forgetful functor from the category of comonads to the category of endofunctors.

instance CategoryTheory.instFaithfulComonadInstCategoryComonadFunctorCategoryComonadToFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Faithful (CategoryTheory.comonadToFunctor C)

theorem CategoryTheory.comonadToFunctor_mapIso_comonad_iso_mk (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (f : M.toFunctor ≅ N.toFunctor) (f_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) ((CategoryTheory.Comonad.ε N).app X) = (CategoryTheory.Comonad.ε M).app X) (f_δ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) ((CategoryTheory.Comonad.δ N).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ M).app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))) : (CategoryTheory.comonadToFunctor C).mapIso (CategoryTheory.ComonadIso.mk f) = f

instance CategoryTheory.instReflectsIsomorphismsComonadInstCategoryComonadFunctorCategoryComonadToFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.comonadToFunctor C)

@[simp]

theorem CategoryTheory.MonadIso.toNatIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Monad C} {N : CategoryTheory.Monad C} (h : M ≅ N) : (CategoryTheory.MonadIso.toNatIso h).inv = h.inv.toNatTrans

@[simp]

theorem CategoryTheory.MonadIso.toNatIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Monad C} {N : CategoryTheory.Monad C} (h : M ≅ N) : (CategoryTheory.MonadIso.toNatIso h).hom = h.hom.toNatTrans

def CategoryTheory.MonadIso.toNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Monad C} {N : CategoryTheory.Monad C} (h : M ≅ N) : M.toFunctor ≅ N.toFunctor

An isomorphism of monads gives a natural isomorphism of the underlying functors.

@[simp]

theorem CategoryTheory.ComonadIso.toNatIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (h : M ≅ N) : (CategoryTheory.ComonadIso.toNatIso h).inv = h.inv.toNatTrans

@[simp]

theorem CategoryTheory.ComonadIso.toNatIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (h : M ≅ N) : (CategoryTheory.ComonadIso.toNatIso h).hom = h.hom.toNatTrans

def CategoryTheory.ComonadIso.toNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {M : CategoryTheory.Comonad C} {N : CategoryTheory.Comonad C} (h : M ≅ N) : M.toFunctor ≅ N.toFunctor

An isomorphism of comonads gives a natural isomorphism of the underlying functors.

@[simp]

theorem CategoryTheory.Monad.id_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.Monad.id C).toFunctor.map f = f

@[simp]

theorem CategoryTheory.Monad.id_μ_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Monad.μ (CategoryTheory.Monad.id C)).app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Monad.id_η_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Monad.η (CategoryTheory.Monad.id C)).app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Monad.id_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Monad.id C).toFunctor.obj X = X

def CategoryTheory.Monad.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Monad C

The identity monad.

instance CategoryTheory.Monad.instInhabitedMonad (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Inhabited (CategoryTheory.Monad C)

@[simp]

theorem CategoryTheory.Comonad.id_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.Comonad.id C).toFunctor.map f = f

@[simp]

theorem CategoryTheory.Comonad.id_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Comonad.id C).toFunctor.obj X = X

@[simp]

theorem CategoryTheory.Comonad.id_ε_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Comonad.ε (CategoryTheory.Comonad.id C)).app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Comonad.id_δ_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Comonad.δ (CategoryTheory.Comonad.id C)).app X = CategoryTheory.CategoryStruct.id X

def CategoryTheory.Comonad.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Comonad C

The identity comonad.

instance CategoryTheory.Comonad.instInhabitedComonad (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Inhabited (CategoryTheory.Comonad C)