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
🔸 coverage
@[implicit_reducible]
instance CategoryTheory.Monad.instMonObjFunctor {C : Type u} [Category.{v, u} C] (M : Monad C) :
MonObj M.toFunctor
source
📐 coverage
@[simp]
theorem CategoryTheory.Monad.mul_def {C : Type u} [Category.{v, u} C] (M : Monad C) :
MonObj.mul = M.μ
source
📐 coverage
@[simp]
theorem CategoryTheory.Monad.one_def {C : Type u} [Category.{v, u} C] (M : Monad C) :
MonObj.one = M.η
source
🔸 coverage
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.

Instances For
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.Monad.toMon_X {C : Type u} [Category.{v, u} C] (M : Monad C) :
    M.toMon.X = M.toFunctor
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.Monad.toMon_mon {C : Type u} [Category.{v, u} C] (M : Monad C) :
    M.toMon.mon = M.instMonObjFunctor
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      @[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
      📐 coverage
      @[simp]
      theorem CategoryTheory.Monad.monadToMon_obj (C : Type u) [Category.{v, u} C] (M : Monad C) :
      (monadToMon C).obj M = M.toMon
      source
      🔸 coverage
      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.

      Instances For
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.Monad.ofMon_η {C : Type u} [Category.{v, u} C] (M : Mon (Functor C C)) :
        (ofMon M).η = MonObj.one
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.Monad.ofMon_μ {C : Type u} [Category.{v, u} C] (M : Mon (Functor C C)) :
        (ofMon M).μ = MonObj.mul
        source
        📐 coverage
        @[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
        🔸 coverage
        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.

        Instances For
          source
          📐 coverage
          @[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
          📐 coverage
          @[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
          🔸 coverage
          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).

          Instances For
            source
            📐 coverage
            @[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
            📐 coverage
            @[simp]
            theorem CategoryTheory.Monad.monadMonEquiv_inverse (C : Type u) [Category.{v, u} C] :
            (monadMonEquiv C).inverse = monToMonad C
            source
            📐 coverage
            @[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
            📐 coverage
            @[simp]
            theorem CategoryTheory.Monad.monadMonEquiv_functor (C : Type u) [Category.{v, u} C] :
            (monadMonEquiv C).functor = monadToMon C
            source
            📐 coverage
            @[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
            📐 coverage
            @[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✝¹)