Documentation

Mathlib.CategoryTheory.Monoidal.Action.End

Actions as monoidal functors to endofunctor categories #

In this file, we show that given a right action of a monoidal category C on a category D, the curried action functor C ⥤ D ⥤ D is monoidal. Conversely, given a monoidal functor C ⥤ D ⥤ D, we can define a right action of C on D.

The corresponding results are also available for left actions: given a left action of C on D, composing CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction C D with CategoryTheory.MonoidalCategory.MonoidalOpposite.mopFunctor (D ⥤ D) is monoidal, and conversely one can define a left action of C on D from a monoidal functor C ⥤ (D ⥤ D)ᴹᵒᵖ.

source
🔸 coverage
def CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] :
Functor C (Functor D D)ᴹᵒᵖ

A variant of CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction that takes value in the monoidal opposite of D ⥤ D.

Equations
    Instances For
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_map (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (X : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
      ((curriedActionMop C D).obj X).unmop.map f = actionHomRight X f
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_obj (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (X : C) (y : D) :
      ((curriedActionMop C D).obj X).unmop.obj y = actionObj X y
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] {c c' : C} (f : c ⟶ c') (d : D) :
      ((curriedActionMop C D).map f).unmop.app d = actionHomLeft f d
      source
      🔸 coverage
      instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] :
      (curriedActionMop C D).Monoidal

      When C acts on the left on D, the functor curriedActionMop : C ⥤ (D ⥤ D)ᴹᵒᵖ is monoidal, where D ⥤ D has the composition monoidal structure.

      Equations
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (X : D) :
        (Functor.LaxMonoidal.ε (curriedActionMop C D)).unmop.app X = (actionUnitIso X).inv
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (X : D) :
        (Functor.OplaxMonoidal.η (curriedActionMop C D)).unmop.app X = (actionUnitIso X).hom
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (x✝ x✝¹ : C) (x✝² : D) :
        (Functor.OplaxMonoidal.δ (curriedActionMop C D) x✝ x✝¹).unmop.app x✝² = (actionAssocIso x✝ x✝¹ x✝²).hom
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (x✝ x✝¹ : C) (x✝² : D) :
        (Functor.LaxMonoidal.μ (curriedActionMop C D) x✝ x✝¹).unmop.app x✝² = (actionAssocIso x✝ x✝¹ x✝²).inv
        source
        🔸 coverage
        def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] :
        MonoidalLeftAction C D

        A monoidal functor F : C ⥤ (D ⥤ D)ᴹᵒᵖ can be thought of as a left action of C on D.

        Equations
          Instances For
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (d : D) :
            (actionUnitIso d).inv = (Functor.LaxMonoidal.ε F).unmop.app d
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d') :
            actionHom f g = CategoryStruct.comp ((F.map f).unmop.app d) ((F.obj c').unmop.map g)
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (c c' : C) (d : D) :
            (actionAssocIso c c' d).inv = (Functor.LaxMonoidal.μ F c c').unmop.app d
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] {c✝ c'✝ : C} (f : c✝ ⟶ c'✝) (d : D) :
            actionHomLeft f d = (F.map f).unmop.app d
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (d : D) :
            (actionUnitIso d).hom = (Functor.OplaxMonoidal.η F).unmop.app d
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (c : C) (x✝ x✝¹ : D) (f : x✝ ⟶ x✝¹) :
            actionHomRight c f = (F.obj c).unmop.map f
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (c c' : C) (d : D) :
            (actionAssocIso c c' d).hom = (Functor.OplaxMonoidal.δ F c c').unmop.app d
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionObj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (c : C) (d : D) :
            actionObj c d = (F.obj c).unmop.obj d
            source
            🔸 coverage
            def CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] :
            curriedActionMop C D ≅ F

            If the (left) action of C on D comes from a monoidal functor C ⥤ (D ⥤ D)ᴹᵒᵖ, then curriedActionMop C D is naturally isomorphic to that functor.

            Equations
              Instances For
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (X : C) (X✝ : D) :
                ((curriedActionActionOfMonoidalFunctorToEndofunctorMopIso F).hom.app X).unmop.app X✝ = CategoryStruct.id ((F.obj X).unmop.obj X✝)
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (X : C) (X✝ : D) :
                ((curriedActionActionOfMonoidalFunctorToEndofunctorMopIso F).inv.app X).unmop.app X✝ = CategoryStruct.id ((F.obj X).unmop.obj X✝)
                source
                🔸 coverage
                instance CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalRightAction C D] :
                (curriedAction C D).Monoidal

                When C acts on the right on D, the functor curriedAction : C ⥤ (D ⥤ D) is monoidal, where D ⥤ D has the composition monoidal structure.

                Equations
                  source
                  📐 coverage
                  @[simp]
                  theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_μ_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalRightAction C D] (x✝ x✝¹ : C) (x✝² : D) :
                  (Functor.LaxMonoidal.μ (curriedAction C D) x✝ x✝¹).app x✝² = (actionAssocIso x✝² x✝ x✝¹).inv
                  source
                  📐 coverage
                  @[simp]
                  theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_δ_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalRightAction C D] (x✝ x✝¹ : C) (x✝² : D) :
                  (Functor.OplaxMonoidal.δ (curriedAction C D) x✝ x✝¹).app x✝² = (actionAssocIso x✝² x✝ x✝¹).hom
                  source
                  📐 coverage
                  @[simp]
                  theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_η_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalRightAction C D] (X : D) :
                  (Functor.OplaxMonoidal.η (curriedAction C D)).app X = (actionUnitIso X).hom
                  source
                  📐 coverage
                  @[simp]
                  theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_ε_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] [MonoidalRightAction C D] (X : D) :
                  (Functor.LaxMonoidal.ε (curriedAction C D)).app X = (actionUnitIso X).inv
                  source
                  🔸 coverage
                  def CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] :
                  MonoidalRightAction C D

                  A monoidal functor F : C ⥤ D ⥤ D can be thought of as a right action of C on D.

                  Equations
                    Instances For
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) :
                      (actionUnitIso d).hom = (Functor.OplaxMonoidal.η F).app d
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) (c c' : C) :
                      (actionAssocIso d c c').inv = (Functor.LaxMonoidal.μ F c c').app d
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) :
                      (actionUnitIso d).inv = (Functor.LaxMonoidal.ε F).app d
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) (c c' : C) :
                      (actionAssocIso d c c').hom = (Functor.OplaxMonoidal.δ F c c').app d
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c') :
                      actionHom f g = CategoryStruct.comp ((F.map g).app d) ((F.obj c').map f)
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) (x✝ x✝¹ : C) (f : x✝ ⟶ x✝¹) :
                      actionHomRight d f = (F.map f).app d
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] {d✝ d'✝ : D} (f : d✝ ⟶ d'✝) (c : C) :
                      actionHomLeft f c = (F.obj c).map f
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionObj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) (c : C) :
                      actionObj d c = (F.obj c).obj d
                      source
                      🔸 coverage
                      def CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] :
                      curriedAction C D ≅ F

                      If the action of C on D comes from a monoidal functor C ⥤ (D ⥤ D), then curriedActionMop C D is naturally isomorphic to that functor.

                      Equations
                        Instances For
                          source
                          📐 coverage
                          @[simp]
                          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso_inv_app_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (X : C) (X✝ : D) :
                          ((curriedActionActionOfMonoidalFunctorToEndofunctorIso F).inv.app X).app X✝ = CategoryStruct.id ((F.obj X).obj X✝)
                          source
                          📐 coverage
                          @[simp]
                          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso_hom_app_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [MonoidalCategory C] [Category.{v_2, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (X : C) (X✝ : D) :
                          ((curriedActionActionOfMonoidalFunctorToEndofunctorIso F).hom.app X).app X✝ = CategoryStruct.id ((F.obj X).obj X✝)
                          source
                          🔸 coverage
                          def CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction (C : Type u_1) [Category.{v_1, u_1} C] :
                          MonoidalRightAction (Functor C C) C

                          Functor evaluation gives a right action of C ⥤ C.

                          Note that in the literature, this is defined as a left action, but mathlib's monoidal structure on C ⥤ C is the monoidal opposite of the one usually considered in the literature.

                          Equations
                            Instances For
                              source
                              📐 coverage
                              @[simp]
                              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso (C : Type u_1) [Category.{v_1, u_1} C] (d : C) (c c' : Functor C C) :
                              MonoidalRightActionStruct.actionAssocIso d c c' = ((Functor.Monoidal.μIso (Functor.id (Functor C C)) c c').app d).symm
                              source
                              📐 coverage
                              @[simp]
                              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomLeft (C : Type u_1) [Category.{v_1, u_1} C] {d✝ d'✝ : C} (f : d✝ ⟶ d'✝) (c : Functor C C) :
                              MonoidalRightActionStruct.actionHomLeft f c = c.map f
                              source
                              📐 coverage
                              @[simp]
                              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionObj (C : Type u_1) [Category.{v_1, u_1} C] (d : C) (c : Functor C C) :
                              MonoidalRightActionStruct.actionObj d c = c.obj d
                              source
                              📐 coverage
                              @[simp]
                              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomRight (C : Type u_1) [Category.{v_1, u_1} C] (d : C) (x✝ x✝¹ : Functor C C) (f : x✝ ⟶ x✝¹) :
                              MonoidalRightActionStruct.actionHomRight d f = f.app d
                              source
                              📐 coverage
                              @[simp]
                              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso (C : Type u_1) [Category.{v_1, u_1} C] (d : C) :
                              MonoidalRightActionStruct.actionUnitIso d = ((Functor.Monoidal.εIso (Functor.id (Functor C C))).app d).symm