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

    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

      The unit for the monad T.

      Instances For

        The multiplication for the monad T.

        Instances For

          The counit for the comonad G.

          Instances For

            The comultiplication for the comonad G.

            Instances For

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

              Instances For

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

                Instances For

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

                  Instances For

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

                    Instances For

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

                      Instances For

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

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

                              Instances For
                                @[simp]
                                @[simp]

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

                                Instances For

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

                                  Instances For

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

                                    Instances For

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

                                      Instances For

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

                                        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).toFunctor.map f = f
                                          @[simp]
                                          @[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