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
def CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_obj (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] (X : C) (y : D) :
    ((curriedActionMop C D).obj X).unmop.obj y = actionObj X y
    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_map (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
    @[simp]
    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
    instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
    • One or more equations did not get rendered due to their size.
    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] (X : D) :
    (Functor.OplaxMonoidal.η (curriedActionMop C D)).unmop.app X = (actionUnitIso X).hom
    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] (X : D) :
    (Functor.LaxMonoidal.ε (curriedActionMop C D)).unmop.app X = (actionUnitIso X).inv
    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
    @[simp]
    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
    def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (d : D) :
      (actionUnitIso d).inv = (Functor.LaxMonoidal.ε F).unmop.app d
      source
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] (F : Functor C (Functor D D)ᴹᵒᵖ) [F.Monoidal] (d : D) :
      (actionUnitIso d).hom = (Functor.OplaxMonoidal.η F).unmop.app d
      source
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
      @[simp]
      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionObj {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
      def CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
        instance CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_ε_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] (X : D) :
        (Functor.LaxMonoidal.ε (curriedAction C D)).app X = (actionUnitIso X).inv
        source
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_η_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] (X : D) :
        (Functor.OplaxMonoidal.η (curriedAction C D)).app X = (actionUnitIso X).hom
        source
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_δ_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
        @[simp]
        theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_μ_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
        def CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
          @[simp]
          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) :
          (actionUnitIso d).hom = (Functor.OplaxMonoidal.η F).app d
          source
          @[simp]
          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) :
          (actionUnitIso d).inv = (Functor.LaxMonoidal.ε F).app d
          source
          @[simp]
          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionObj {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] (F : Functor C (Functor D D)) [F.Monoidal] (d : D) (c : C) :
          actionObj d c = (F.obj c).obj d
          source
          @[simp]
          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
          @[simp]
          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
          @[simp]
          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
          @[simp]
          theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
          def CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso_inv_app_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
            @[simp]
            theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso_hom_app_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, 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
            def CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction (C : Type u_1) [Category.{u_3, 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
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomLeft (C : Type u_1) [Category.{u_3, u_1} C] {d✝ d'✝ : C} (f : d✝ ⟶ d'✝) (c : Functor C C) :
              MonoidalRightActionStruct.actionHomLeft f c = c.map f
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomRight (C : Type u_1) [Category.{u_3, u_1} C] (d : C) (x✝ x✝¹ : Functor C C) (f : x✝ ⟶ x✝¹) :
              MonoidalRightActionStruct.actionHomRight d f = f.app d
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso (C : Type u_1) [Category.{u_3, 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
              @[simp]
              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionObj (C : Type u_1) [Category.{u_3, u_1} C] (d : C) (c : Functor C C) :
              MonoidalRightActionStruct.actionObj d c = c.obj d
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso (C : Type u_1) [Category.{u_3, u_1} C] (d : C) :
              MonoidalRightActionStruct.actionUnitIso d = ((Functor.Monoidal.εIso (Functor.id (Functor C C))).app d).symm