Documentation

Mathlib.CategoryTheory.Monad.EquivMon

The equivalence between Monad C and Mon_ (C ⥤ C). #

A monad "is just" a monoid in the category of endofunctors.

Definitions/Theorems #

  1. toMon associates a monoid object in C ⥤ C to any monad on C.
  2. monadToMon is the functorial version of toMon.
  3. ofMon associates a monad on C to any monoid object in C ⥤ C.
  4. monadMonEquiv is the equivalence between Monad C and Mon_ (C ⥤ C).
source
def CategoryTheory.Monad.toMon {C : Type u} [Category.{v, u} C] (M : Monad C) :
Mon_ (Functor C C)

To every Monad C we associated a monoid object in C ⥤ C.

Equations
  • M.toMon = { X := M.toFunctor, one := M.η, mul := M.μ, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
Instances For
    source
    @[simp]
    theorem CategoryTheory.Monad.toMon_mul {C : Type u} [Category.{v, u} C] (M : Monad C) :
    M.toMon.mul = M.μ
    source
    @[simp]
    theorem CategoryTheory.Monad.toMon_one {C : Type u} [Category.{v, u} C] (M : Monad C) :
    M.toMon.one = M.η
    source
    @[simp]
    theorem CategoryTheory.Monad.toMon_X {C : Type u} [Category.{v, u} C] (M : Monad C) :
    M.toMon.X = M.toFunctor
    source
    def CategoryTheory.Monad.monadToMon (C : Type u) [Category.{v, u} C] :
    Functor (Monad C) (Mon_ (Functor C C))

    Passing from Monad C to Mon_ (C ⥤ C) is functorial.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Monad.monadToMon_map_hom (C : Type u) [Category.{v, u} C] {X✝ Y✝ : Monad C} (f : X✝ ⟶ Y✝) :
      ((monadToMon C).map f).hom = f.toNatTrans
      source
      @[simp]
      theorem CategoryTheory.Monad.monadToMon_obj (C : Type u) [Category.{v, u} C] (M : Monad C) :
      (monadToMon C).obj M = M.toMon
      source
      def CategoryTheory.Monad.ofMon {C : Type u} [Category.{v, u} C] (M : Mon_ (Functor C C)) :
      Monad C

      To every monoid object in C ⥤ C we associate a Monad C.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Monad.ofMon_η {C : Type u} [Category.{v, u} C] (M : Mon_ (Functor C C)) :
        (ofMon M).η = M.one
        source
        @[simp]
        theorem CategoryTheory.Monad.ofMon_μ {C : Type u} [Category.{v, u} C] (M : Mon_ (Functor C C)) :
        (ofMon M).μ = M.mul
        source
        @[simp]
        theorem CategoryTheory.Monad.ofMon_obj {C : Type u} [Category.{v, u} C] (M : Mon_ (Functor C C)) (X : C) :
        (ofMon M).obj X = M.X.obj X
        source
        def CategoryTheory.Monad.monToMonad (C : Type u) [Category.{v, u} C] :
        Functor (Mon_ (Functor C C)) (Monad C)

        Passing from Mon_ (C ⥤ C) to Monad C is functorial.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Monad.monToMonad_obj (C : Type u) [Category.{v, u} C] (M : Mon_ (Functor C C)) :
          (monToMonad C).obj M = ofMon M
          source
          @[simp]
          theorem CategoryTheory.Monad.monToMonad_map_toNatTrans (C : Type u) [Category.{v, u} C] {X Y : Mon_ (Functor C C)} (f : X ⟶ Y) :
          ((monToMonad C).map f).toNatTrans = f.hom
          source
          def CategoryTheory.Monad.monadMonEquiv (C : Type u) [Category.{v, u} C] :
          Monad C ≌ Mon_ (Functor C C)

          Oh, monads are just monoids in the category of endofunctors (equivalence of categories).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app (C : Type u) [Category.{v, u} C] (x✝ : Monad C) (x✝¹ : C) :
            ((monadMonEquiv C).unitIso.hom.app x✝).app x✝¹ = CategoryStruct.id (((Functor.id (Monad C)).obj x✝).obj x✝¹)
            source
            @[simp]
            theorem CategoryTheory.Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app (C : Type u) [Category.{v, u} C] (x✝ : Monad C) (x✝¹ : C) :
            ((monadMonEquiv C).unitIso.inv.app x✝).app x✝¹ = CategoryStruct.id ((((monadToMon C).comp (monToMonad C)).obj x✝).obj x✝¹)
            source
            @[simp]
            theorem CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom (C : Type u) [Category.{v, u} C] (x✝ : Mon_ (Functor C C)) :
            ((monadMonEquiv C).counitIso.inv.app x✝).hom = CategoryStruct.id ((Functor.id (Mon_ (Functor C C))).obj x✝).X
            source
            @[simp]
            theorem CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom (C : Type u) [Category.{v, u} C] (x✝ : Mon_ (Functor C C)) :
            ((monadMonEquiv C).counitIso.hom.app x✝).hom = CategoryStruct.id (((monToMonad C).comp (monadToMon C)).obj x✝).X
            source
            @[simp]
            theorem CategoryTheory.Monad.monadMonEquiv_inverse (C : Type u) [Category.{v, u} C] :
            (monadMonEquiv C).inverse = monToMonad C
            source
            @[simp]
            theorem CategoryTheory.Monad.monadMonEquiv_functor (C : Type u) [Category.{v, u} C] :
            (monadMonEquiv C).functor = monadToMon C