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₁)

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)

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

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

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

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

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

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)

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

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

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

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

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

Equations

• CategoryTheory.coeMonad = { coe := fun (T : CategoryTheory.Monad C) => T.toFunctor }

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

Equations

• CategoryTheory.coeComonad = { coe := fun (G : CategoryTheory.Comonad C) => G.toFunctor }

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.

Equations

• T.η = T.η'

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

The multiplication for the monad T.

Equations

• T.μ = 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.

Equations

• G.ε = G.ε'

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

The comultiplication for the comonad G.

Equations

• G.δ = 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.

Equations

• CategoryTheory.Monad.Simps.coe T = T.toFunctor

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.

Equations

• CategoryTheory.Monad.Simps.η T = T.η

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

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

Equations

• CategoryTheory.Monad.Simps.μ T = T.μ

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.

Equations

• CategoryTheory.Comonad.Simps.coe G = G.toFunctor

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.

Equations

• CategoryTheory.Comonad.Simps.ε G = G.ε

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

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

Equations

• CategoryTheory.Comonad.Simps.δ G = G.δ

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 (T.μ.app X)) (CategoryTheory.CategoryStruct.comp (T.μ.app X) h) = CategoryTheory.CategoryStruct.comp (T.μ.app (T.obj X)) (CategoryTheory.CategoryStruct.comp (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 (T.μ.app X)) (T.μ.app X) = CategoryTheory.CategoryStruct.comp (T.μ.app (T.obj X)) (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 (T.η.app (T.obj X)) (CategoryTheory.CategoryStruct.comp (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 (T.η.app (T.obj X)) (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 (T.η.app X)) (CategoryTheory.CategoryStruct.comp (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 (T.η.app X)) (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 (G.obj (G.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.δ.app X) (CategoryTheory.CategoryStruct.comp (G.map (G.δ.app X)) h) = CategoryTheory.CategoryStruct.comp (G.δ.app X) (CategoryTheory.CategoryStruct.comp (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 (G.δ.app X) (G.map (G.δ.app X)) = CategoryTheory.CategoryStruct.comp (G.δ.app X) (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 : G.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.δ.app X) (CategoryTheory.CategoryStruct.comp (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 (G.δ.app X) (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 X ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.δ.app X) (CategoryTheory.CategoryStruct.comp (G.map (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 (G.δ.app X) (G.map (G.ε.app X)) = CategoryTheory.CategoryStruct.id (G.obj X)

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

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

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₁)

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

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

@[simp]

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

@[simp]

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

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

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

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₁)

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

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

@[simp]

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

@[simp]

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

@[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 (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 (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 (T₁.η.app X) (CategoryTheory.CategoryStruct.comp (self.app X) h) = CategoryTheory.CategoryStruct.comp (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 : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (N.ε.app X) h) = CategoryTheory.CategoryStruct.comp (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 : N.obj (N.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (N.δ.app X) h) = CategoryTheory.CategoryStruct.comp (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)

Equations

• CategoryTheory.instQuiverMonad = { Hom := CategoryTheory.MonadHom }

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

Equations

• CategoryTheory.instQuiverComonad = { Hom := CategoryTheory.ComonadHom }

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)

Equations

• CategoryTheory.instCategoryMonad = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

Equations

• CategoryTheory.instCategoryComonad = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

Equations

• CategoryTheory.instInhabitedMonadHom = { default := CategoryTheory.CategoryStruct.id 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)

Equations

• CategoryTheory.instInhabitedComonadHom = { default := CategoryTheory.CategoryStruct.id 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 (M.η.app X) (f.hom.app X) = N.η.app X) _auto✝) (f_μ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (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))) (N.μ.app X)) _auto✝) : (CategoryTheory.MonadIso.mk f f_η 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 (M.η.app X) (f.hom.app X) = N.η.app X) _auto✝) (f_μ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (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))) (N.μ.app X)) _auto✝) : (CategoryTheory.MonadIso.mk f f_η 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 (M.η.app X) (f.hom.app X) = N.η.app X) _auto✝) (f_μ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (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))) (N.μ.app X)) _auto✝) : M ≅ N

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

Equations

• CategoryTheory.MonadIso.mk f f_η f_μ = { hom := { toNatTrans := f.hom, app_η := f_η, app_μ := f_μ }, inv := { toNatTrans := f.inv, app_η := ⋯, app_μ := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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) (N.ε.app X) = M.ε.app X) _auto✝) (f_δ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) = CategoryTheory.CategoryStruct.comp (M.δ.app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))) _auto✝) : (CategoryTheory.ComonadIso.mk f f_ε 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) (N.ε.app X) = M.ε.app X) _auto✝) (f_δ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) = CategoryTheory.CategoryStruct.comp (M.δ.app X) (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))) _auto✝) : (CategoryTheory.ComonadIso.mk f f_ε 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) (N.ε.app X) = M.ε.app X) _auto✝) (f_δ : autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) = CategoryTheory.CategoryStruct.comp (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.

Equations

• CategoryTheory.ComonadIso.mk f f_ε f_δ = { hom := { toNatTrans := f.hom, app_ε := f_ε, app_δ := f_δ }, inv := { toNatTrans := f.inv, app_ε := ⋯, app_δ := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

Equations

• CategoryTheory.monadToFunctor C = { obj := fun (T : CategoryTheory.Monad C) => T.toFunctor, map := fun {X Y : CategoryTheory.Monad C} (f : X ⟶ Y) => f.toNatTrans, map_id := ⋯, map_comp := ⋯ }

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

Equations

• ⋯ = ⋯

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 (M.η.app X) (f.hom.app X) = N.η.app X) (f_μ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (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))) (N.μ.app X)) : (CategoryTheory.monadToFunctor C).mapIso (CategoryTheory.MonadIso.mk f f_η f_μ) = f

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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) (N.ε.app X) = M.ε.app X) (f_δ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) = CategoryTheory.CategoryStruct.comp (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_ε f_δ) = f

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.MonadIso.toNatIso h = (CategoryTheory.monadToFunctor C).mapIso h

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

Equations

• CategoryTheory.ComonadIso.toNatIso h = (CategoryTheory.comonadToFunctor C).mapIso h

@[simp]

theorem CategoryTheory.Monad.id_μ_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (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.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).obj X = X

@[simp]

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

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

The identity monad.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Monad.instInhabited C = { default := CategoryTheory.Monad.id 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).map f = f

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Comonad.id_ε_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Comonad.instInhabited C = { default := CategoryTheory.Comonad.id C }

def CategoryTheory.Monad.transport {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C C} (T : CategoryTheory.Monad C) (i : T.toFunctor ≅ F) : CategoryTheory.Monad C

Transport a monad structure on a functor along an isomorphism of functors.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Comonad.transport {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C C} (T : CategoryTheory.Comonad C) (i : T.toFunctor ≅ F) : CategoryTheory.Comonad C

Transport a comonad structure on a functor along an isomorphism of functors.

Equations

• One or more equations did not get rendered due to their size.