Documentation

Mathlib.CategoryTheory.Monad.Basic

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.

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)
Instances For
    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)

    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)
    Instances For
      @[simp]
      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))
      @[simp]
      Equations
      Equations
      @[simp]
      theorem CategoryTheory.Monad.right_unit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Monad C) (X : C) {Z : C} (h : self.obj X Z) :
      CategoryTheory.CategoryStruct.comp (self.map (self.app X)) (CategoryTheory.CategoryStruct.comp (self.app X) h) = h
      @[simp]
      theorem CategoryTheory.Monad.left_unit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Monad C) (X : C) {Z : C} (h : self.obj X Z) :
      CategoryTheory.CategoryStruct.comp (self.app (self.obj X)) (CategoryTheory.CategoryStruct.comp (self.app X) h) = h
      @[simp]
      theorem CategoryTheory.Comonad.left_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C) {Z : C} (h : self.obj X Z) :
      CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (self.app (self.obj X)) h) = h
      @[simp]
      theorem CategoryTheory.Comonad.coassoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C) {Z : C} (h : self.obj (self.obj (self.obj X)) Z) :
      CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (self.map (self.app X)) h) = CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (self.app (self.obj X)) h)
      @[simp]
      theorem CategoryTheory.Comonad.right_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C) {Z : C} (h : self.obj X Z) :
      CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (self.map (self.app X)) h) = h
      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.appx = y

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

      Instances For
        @[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 {C : Type u₁} :
        ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {M N : CategoryTheory.Comonad C} {x y : CategoryTheory.ComonadHom M N}, x.app = y.appx = y

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

        Instances For
          @[simp]
          @[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) :
          Equations
          • CategoryTheory.instQuiverMonad = { Hom := CategoryTheory.MonadHom }
          Equations
          • CategoryTheory.instQuiverComonad = { Hom := CategoryTheory.ComonadHom }
          theorem CategoryTheory.MonadHom.ext'_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} {f : T₁ T₂} {g : T₁ T₂} :
          f = g f.app = g.app
          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'_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Comonad C} {T₂ : CategoryTheory.Comonad C} {f : T₁ T₂} {g : T₁ T₂} :
          f = g f.app = g.app
          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
          @[simp]
          @[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₃) :
          @[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
          @[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
          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 := }
          Instances For
            @[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
            @[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
            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 := }
            Instances For

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

              Equations
              Instances For
                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)) :

                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.
                Instances For
                  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)))) :

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

                  Equations
                  Instances For

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

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

                      The identity monad.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[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

                        The identity comonad.

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

                          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.
                          Instances For

                            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.
                            Instances For