Documentation

Mathlib.CategoryTheory.Monoidal.Action.Basic

Left actions from a monoidal category on a category #

Given a monoidal category C, and a category D, we define a left action of C on D as the data of an object c ⊙ₗ d of D for every c : C and d : D, as well as the data required to turn - ⊙ₗ - into a bifunctor, along with structure natural isomorphisms (- ⊗ -) ⊙ₗ - ≅ - ⊙ₗ - ⊙ₗ - and 𝟙_ C ⊙ₗ - ≅ -, subject to coherence conditions.

References #

TODOs/Projects #

source
class CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategoryStruct C] :
Type (max (max (max u_1 u_2) u_3) u_4)

A class that carries the non-Prop data required to define a left action of a monoidal category C on a category D, to set up notations.

  • actionObj : C → D → D

    The left action on objects. This is denoted c ⊙ₗ d.

  • actionHomLeft {c c' : C} (f : c ⟶ c') (d : D) : actionObj c d ⟶ actionObj c' d

    The left action of a map f : c ⟶ c' in C on an object d in D. If we are to consider the action as a functor Α : C ⥤ D ⥤ D, this is (Α.map f).app d. This is denoted f ⊵ₗ d`

  • actionHomRight (c : C) {d d' : D} (f : d ⟶ d') : actionObj c d ⟶ actionObj c d'

    The action of an object c : C on a map f : d ⟶ d' in D. If we are to consider the action as a functor Α : C ⥤ D ⥤ D, this is (Α.obj c).map f. This is denoted c ⊴ₗ f`.

  • actionHom {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d') : actionObj c d ⟶ actionObj c' d'

    The action of a pair of maps f : c ⟶ c' and d ⟶ d'. By default, this is defined in terms of actionHomLeft and actionHomRight.

  • actionAssocIso (c c' : C) (d : D) : actionObj (tensorObj c c') d ≅ actionObj c (actionObj c' d)

    The structural isomorphism (c ⊗ c') ⊙ₗ d ≅ c ⊙ₗ (c' ⊙ₗ d).

  • actionUnitIso (d : D) : actionObj (tensorUnit C) d ≅ d

    The structural isomorphism between 𝟙_ C ⊙ₗ d and d.

Instances
    source
    def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊙ₗ_» :
    Lean.TrailingParserDescr

    Notation for actionObj, the action of C on D.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊵ₗ_» :
      Lean.TrailingParserDescr

      Notation for actionHomLeft, the action of C on morphisms in D.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊴ₗ_» :
        Lean.TrailingParserDescr

        Notation for actionHomRight, the action of morphism in C on D.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊙ₗₘ_» :
          Lean.TrailingParserDescr

          Notation for actionHom, the bifunctorial action of morphisms in C and D on - ⊙ₗ -.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def CategoryTheory.MonoidalCategory.MonoidalLeftAction.termαₗ :
            Lean.ParserDescr

            Notation for actionAssocIso, the structural isomorphism - ⊗ - ⊙ₗ - ≅ - ⊙ₗ - ⊙ₗ -.

            Equations
            Instances For
              source
              def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«termλₗ» :
              Lean.ParserDescr

              Notation for actionUnitIso, the structural isomorphism 𝟙_ C ⊙ₗ - ≅ -.

              Equations
              Instances For
                source
                def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«termλₗ[_]» :
                Lean.ParserDescr

                Notation for actionUnitIso, the structural isomorphism 𝟙_ C ⊙ₗ - ≅ -, allowing one to specify the acting category.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  class CategoryTheory.MonoidalCategory.MonoidalLeftAction (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] extends CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D :
                  Type (max (max (max u_1 u_2) u_3) u_4)

                  A MonoidalLeftAction C D is is the data of:

                  • For every object c : C and d : D, an object c ⊙ₗ d of D.
                  • For every morphism f : (c : C) ⟶ c' and every d : D, a morphism f ⊵ₗ d : c ⊙ₗ d ⟶ c' ⊙ₗ d.
                  • For every morphism f : (d : D) ⟶ d' and every c : C, a morphism c ⊴ₗ f : c ⊙ₗ d ⟶ c ⊙ₗ d'.
                  • For every pair of morphisms f : (c : C) ⟶ c' and f : (d : D) ⟶ d', a morphism f ⊙ₗ f' : c ⊙ₗ d ⟶ c' ⊙ₗ d'.
                  • A structure isomorphism αₗ c c' d : c ⊗ c' ⊙ₗ d ≅ c ⊙ₗ c' ⊙ₗ d.
                  • A structure isomorphism λₗ d : (𝟙_ C) ⊙ₗ d ≅ d. Furthermore, we require identities that turn - ⊙ₗ - into a bifunctor, ensure naturality of αₗ and λₗ, and ensure compatibilies with the associator and unitor isomorphisms in C.
                  Instances
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d') {Z : D} (h : actionObj c' d' ⟶ Z) :
                    CategoryStruct.comp (actionHom f g) h = CategoryStruct.comp (actionHomLeft f d) (CategoryStruct.comp (actionHomRight c' g) h)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] (c : C) (d : D) {Z : D} (h : actionObj c d ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft (CategoryStruct.id c) d) h = h
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] (c : C) (d : D) {Z : D} (h : actionObj c d ⟶ Z) :
                    CategoryStruct.comp (actionHomRight c (CategoryStruct.id d)) h = h
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D) {Z : D} (h : actionObj (tensorObj c c'') d ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft (whiskerLeft c f) d) h = CategoryStruct.comp (actionAssocIso c c' d).hom (CategoryStruct.comp (actionHomRight c (actionHomLeft f d)) (CategoryStruct.comp (actionAssocIso c c'' d).inv h))
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] {c c' c'' : C} {d d' d'' : D} (f₁ : c ⟶ c') (f₂ : c' ⟶ c'') (g₁ : d ⟶ d') (g₂ : d' ⟶ d'') {Z : D} (h : actionObj c'' d'' ⟶ Z) :
                    CategoryStruct.comp (actionHom (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂)) h = CategoryStruct.comp (actionHom f₁ g₁) (CategoryStruct.comp (actionHom f₂ g₂) h)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂) (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂) {Z : D} (h✝ : actionObj c₂ (actionObj c₄ d₂) ⟶ Z) :
                    CategoryStruct.comp (actionHom (tensorHom f g) h) (CategoryStruct.comp (actionAssocIso c₂ c₄ d₂).hom h✝) = CategoryStruct.comp (actionAssocIso c₁ c₃ d₁).hom (CategoryStruct.comp (actionHom f (actionHom g h)) h✝)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] {d d' : D} (f : d ⟶ d') {Z : D} (h : d' ⟶ Z) :
                    CategoryStruct.comp (actionUnitIso d).hom (CategoryStruct.comp f h) = CategoryStruct.comp (actionHomRight (tensorUnit C) f) (CategoryStruct.comp (actionUnitIso d').hom h)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] (c₁ c₂ c₃ : C) (d : D) {Z : D} (h : actionObj c₁ (actionObj c₂ (actionObj c₃ d)) ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft (associator c₁ c₂ c₃).hom d) (CategoryStruct.comp (actionAssocIso c₁ (tensorObj c₂ c₃) d).hom (CategoryStruct.comp (actionHomRight c₁ (actionAssocIso c₂ c₃ d).hom) h)) = CategoryStruct.comp (actionAssocIso (tensorObj c₁ c₂) c₃ d).hom (CategoryStruct.comp (actionAssocIso c₁ c₂ (actionObj c₃ d)).hom h)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] (c : C) (d : D) {Z : D} (h : actionObj c d ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft (leftUnitor c).hom d) h = CategoryStruct.comp (actionAssocIso (tensorUnit C) c d).hom (CategoryStruct.comp (actionUnitIso (actionObj c d)).hom h)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalLeftAction C D] (c : C) (d : D) {Z : D} (h : actionObj c d ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft (rightUnitor c).hom d) h = CategoryStruct.comp (actionAssocIso c (tensorUnit C) d).hom (CategoryStruct.comp (actionHomRight c (actionUnitIso d).hom) h)
                    source
                    instance CategoryTheory.MonoidalCategory.selfAction (C : Type u_1) [Category.{u_3, u_1} C] [MonoidalCategory C] :
                    MonoidalLeftAction C C

                    A monoidal category acts on itself through the tensor product.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.selfAction_actionHomRight (C : Type u_1) [Category.{u_3, u_1} C] [MonoidalCategory C] (x x✝ x✝¹ : C) (f : x✝ ⟶ x✝¹) :
                    MonoidalLeftActionStruct.actionHomRight x f = whiskerLeft x f
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.selfAction_actionHomLeft (C : Type u_1) [Category.{u_3, u_1} C] [MonoidalCategory C] {c✝ c'✝ : C} (f : c✝ ⟶ c'✝) (x : C) :
                    MonoidalLeftActionStruct.actionHomLeft f x = whiskerRight f x
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.selfAction_actionHom (C : Type u_1) [Category.{u_3, u_1} C] [MonoidalCategory C] {c✝ c'✝ d✝ d'✝ : C} (f : c✝ ⟶ c'✝) (g : d✝ ⟶ d'✝) :
                    MonoidalLeftActionStruct.actionHom f g = tensorHom f g
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.selfAction_actionObj (C : Type u_1) [Category.{u_3, u_1} C] [MonoidalCategory C] (x y : C) :
                    MonoidalLeftActionStruct.actionObj x y = tensorObj x y
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.selfAction_actionAssocIso (C : Type u_1) [Category.{u_3, u_1} C] [MonoidalCategory C] (x y z : C) :
                    MonoidalLeftActionStruct.actionAssocIso x y z = associator x y z
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.selfAction_actionUnitIso (C : Type u_1) [Category.{u_3, u_1} C] [MonoidalCategory C] (x : C) :
                    MonoidalLeftActionStruct.actionUnitIso x = leftUnitor x
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHom {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (c : C) {d d' : D} (f : d ⟶ d') :
                    actionHom (CategoryStruct.id c) f = actionHomRight c f
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_id {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {c c' : C} (f : c ⟶ c') (d : D) :
                    actionHom f (CategoryStruct.id d) = actionHomLeft f d
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (w : C) {x y z : D} (f : x ⟶ y) (g : y ⟶ z) :
                    actionHomRight w (CategoryStruct.comp f g) = CategoryStruct.comp (actionHomRight w f) (actionHomRight w g)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (w : C) {x y z : D} (f : x ⟶ y) (g : y ⟶ z) {Z : D} (h : actionObj w z ⟶ Z) :
                    CategoryStruct.comp (actionHomRight w (CategoryStruct.comp f g)) h = CategoryStruct.comp (actionHomRight w f) (CategoryStruct.comp (actionHomRight w g) h)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : D} (f : x ⟶ y) :
                    actionHomRight (tensorUnit C) f = CategoryStruct.comp (actionUnitIso x).hom (CategoryStruct.comp f (actionUnitIso y).inv)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : D} (f : x ⟶ y) {Z : D} (h : actionObj (tensorUnit C) y ⟶ Z) :
                    CategoryStruct.comp (actionHomRight (tensorUnit C) f) h = CategoryStruct.comp (actionUnitIso x).hom (CategoryStruct.comp f (CategoryStruct.comp (actionUnitIso y).inv h))
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x y : C) {z z' : D} (f : z ⟶ z') :
                    actionHomRight (tensorObj x y) f = CategoryStruct.comp (actionAssocIso x y z).hom (CategoryStruct.comp (actionHomRight x (actionHomRight y f)) (actionAssocIso x y z').inv)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x y : C) {z z' : D} (f : z ⟶ z') {Z : D} (h : actionObj (tensorObj x y) z' ⟶ Z) :
                    CategoryStruct.comp (actionHomRight (tensorObj x y) f) h = CategoryStruct.comp (actionAssocIso x y z).hom (CategoryStruct.comp (actionHomRight x (actionHomRight y f)) (CategoryStruct.comp (actionAssocIso x y z').inv h))
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {w x y : C} (f : w ⟶ x) (g : x ⟶ y) (z : D) :
                    actionHomLeft (CategoryStruct.comp f g) z = CategoryStruct.comp (actionHomLeft f z) (actionHomLeft g z)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {w x y : C} (f : w ⟶ x) (g : x ⟶ y) (z : D) {Z : D} (h : actionObj y z ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft (CategoryStruct.comp f g) z) h = CategoryStruct.comp (actionHomLeft f z) (CategoryStruct.comp (actionHomLeft g z) h)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x x' : C} (f : x ⟶ x') (y : C) (z : D) :
                    actionHomLeft f (actionObj y z) = CategoryStruct.comp (actionAssocIso x y z).inv (CategoryStruct.comp (actionHomLeft (whiskerRight f y) z) (actionAssocIso x' y z).hom)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x x' : C} (f : x ⟶ x') (y : C) (z : D) {Z : D} (h : actionObj x' (actionObj y z) ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft f (actionObj y z)) h = CategoryStruct.comp (actionAssocIso x y z).inv (CategoryStruct.comp (actionHomLeft (whiskerRight f y) z) (CategoryStruct.comp (actionAssocIso x' y z).hom h))
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {w x : C} {y z : D} (f : w ⟶ x) (g : y ⟶ z) :
                    CategoryStruct.comp (actionHomRight w g) (actionHomLeft f z) = CategoryStruct.comp (actionHomLeft f y) (actionHomRight x g)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {w x : C} {y z : D} (f : w ⟶ x) (g : y ⟶ z) {Z : D} (h : actionObj x z ⟶ Z) :
                    CategoryStruct.comp (actionHomRight w g) (CategoryStruct.comp (actionHomLeft f z) h) = CategoryStruct.comp (actionHomLeft f y) (CategoryStruct.comp (actionHomRight x g) h)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def' {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x₁ y₁ : C} {x₂ y₂ : D} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂) :
                    actionHom f g = CategoryStruct.comp (actionHomRight x₁ g) (actionHomLeft f y₂)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x₁ y₁ : C} {x₂ y₂ : D} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂) {Z : D} (h : actionObj y₁ y₂ ⟶ Z) :
                    CategoryStruct.comp (actionHom f g) h = CategoryStruct.comp (actionHomRight x₁ g) (CategoryStruct.comp (actionHomLeft f y₂) h)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂) (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂) :
                    CategoryStruct.comp (actionHom f (actionHom g h)) (actionAssocIso c₂ c₄ d₂).inv = CategoryStruct.comp (actionAssocIso c₁ c₃ d₁).inv (actionHom (tensorHom f g) h)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂) (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂) {Z : D} (h✝ : actionObj (tensorObj c₂ c₄) d₂ ⟶ Z) :
                    CategoryStruct.comp (actionHom f (actionHom g h)) (CategoryStruct.comp (actionAssocIso c₂ c₄ d₂).inv h✝) = CategoryStruct.comp (actionAssocIso c₁ c₃ d₁).inv (CategoryStruct.comp (actionHom (tensorHom f g) h) h✝)
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {d d' : D} (f : d ⟶ d') :
                    CategoryStruct.comp (actionUnitIso d).inv (actionHomRight (tensorUnit C) f) = CategoryStruct.comp f (actionUnitIso d').inv
                    source
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {d d' : D} (f : d ⟶ d') {Z : D} (h : actionObj (tensorUnit C) d' ⟶ Z) :
                    CategoryStruct.comp (actionUnitIso d).inv (CategoryStruct.comp (actionHomRight (tensorUnit C) f) h) = CategoryStruct.comp f (CategoryStruct.comp (actionUnitIso d').inv h)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ≅ z) :
                    CategoryStruct.comp (actionHomRight x f.hom) (actionHomRight x f.inv) = CategoryStruct.id (actionObj x y)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ≅ z) {Z : D} (h : actionObj x y ⟶ Z) :
                    CategoryStruct.comp (actionHomRight x f.hom) (CategoryStruct.comp (actionHomRight x f.inv) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ≅ y) (z : D) :
                    CategoryStruct.comp (actionHomLeft f.hom z) (actionHomLeft f.inv z) = CategoryStruct.id (actionObj x z)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ≅ y) (z : D) {Z : D} (h : actionObj x z ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft f.hom z) (CategoryStruct.comp (actionHomLeft f.inv z) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ≅ z) :
                    CategoryStruct.comp (actionHomRight x f.inv) (actionHomRight x f.hom) = CategoryStruct.id (actionObj x z)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ≅ z) {Z : D} (h : actionObj x z ⟶ Z) :
                    CategoryStruct.comp (actionHomRight x f.inv) (CategoryStruct.comp (actionHomRight x f.hom) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ≅ y) (z : D) :
                    CategoryStruct.comp (actionHomLeft f.inv z) (actionHomLeft f.hom z) = CategoryStruct.id (actionObj y z)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ≅ y) (z : D) {Z : D} (h : actionObj y z ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft f.inv z) (CategoryStruct.comp (actionHomLeft f.hom z) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z) [IsIso f] :
                    CategoryStruct.comp (actionHomRight x f) (actionHomRight x (inv f)) = CategoryStruct.id (actionObj x y)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv'_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z) [IsIso f] {Z : D} (h : actionObj x y ⟶ Z) :
                    CategoryStruct.comp (actionHomRight x f) (CategoryStruct.comp (actionHomRight x (inv f)) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft' {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ⟶ y) [IsIso f] (z : D) :
                    CategoryStruct.comp (actionHomLeft f z) (actionHomLeft (inv f) z) = CategoryStruct.id (actionObj x z)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft'_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ⟶ y) [IsIso f] (z : D) {Z : D} (h : actionObj x z ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft f z) (CategoryStruct.comp (actionHomLeft (inv f) z) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z) [IsIso f] :
                    CategoryStruct.comp (actionHomRight x (inv f)) (actionHomRight x f) = CategoryStruct.id (actionObj x z)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom'_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z) [IsIso f] {Z : D} (h : actionObj x z ⟶ Z) :
                    CategoryStruct.comp (actionHomRight x (inv f)) (CategoryStruct.comp (actionHomRight x f) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft' {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ⟶ y) [IsIso f] (z : D) :
                    CategoryStruct.comp (actionHomLeft (inv f) z) (actionHomLeft f z) = CategoryStruct.id (actionObj y z)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft'_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ⟶ y) [IsIso f] (z : D) {Z : D} (h : actionObj y z ⟶ Z) :
                    CategoryStruct.comp (actionHomLeft (inv f) z) (CategoryStruct.comp (actionHomLeft f z) h) = h
                    source
                    instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z) [IsIso f] :
                    IsIso (actionHomRight x f)
                    source
                    instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ⟶ y) [IsIso f] (z : D) :
                    IsIso (actionHomLeft f z)
                    source
                    instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} {x' y' : D} (f : x ⟶ y) (g : x' ⟶ y') [IsIso f] [IsIso g] :
                    IsIso (actionHom f g)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ⟶ y) [IsIso f] (z : D) :
                    inv (actionHomLeft f z) = actionHomLeft (inv f) z
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z) [IsIso f] :
                    inv (actionHomRight x f) = actionHomRight x (inv f)
                    source
                    @[simp]
                    theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} {x' y' : D} (f : x ⟶ y) (g : x' ⟶ y') [IsIso f] [IsIso g] :
                    inv (actionHom f g) = actionHom (inv f) (inv g)
                    source
                    def CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] :
                    Functor C (Functor D D)

                    Bundle the action of C on D as a functor C ⥤ D ⥤ D.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_obj_obj (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) (y : D) :
                      ((curriedAction C D).obj x).obj y = actionObj x y
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_map_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (y : D) :
                      ((curriedAction C D).map f).app y = actionHomLeft f y
                      source
                      @[simp]
                      theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_obj_map (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
                      ((curriedAction C D).obj x).map f = actionHomRight x f
                      source
                      @[reducible, inline]
                      abbrev CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft {C : Type u_1} (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (c : C) :
                      Functor D D

                      Bundle d ↦ c ⊙ₗ d as a functor.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft_obj {C : Type u_1} (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (c : C) (y : D) :
                        (actionLeft D c).obj y = actionObj c y
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft_map {C : Type u_1} (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (c : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
                        (actionLeft D c).map f = actionHomRight c f
                        source
                        @[reducible, inline]
                        abbrev CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight (C : Type u_1) {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (d : D) :
                        Functor C D

                        Bundle c ↦ c ⊙ₗ d as a functor.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight_obj (C : Type u_1) {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (d : D) (j : C) :
                          (actionRight C d).obj j = actionObj j d
                          source
                          @[simp]
                          theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight_map (C : Type u_1) {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (d : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                          (actionRight C d).map f = actionHomLeft f d
                          source
                          def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] :
                          bifunctorComp₁₂ (curriedTensor C) (curriedAction C D) ≅ bifunctorComp₂₃ (curriedAction C D) (curriedAction C D)

                          Bundle αₗ _ _ _ as an isomorphism of trifunctors.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_hom_app_app_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (X X✝ : C) (X✝ : D) :
                            (((actionAssocNatIso C D).hom.app X).app X✝).app X✝ = (actionAssocIso X X✝ X✝).hom
                            source
                            @[simp]
                            theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_inv_app_app_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (X X✝ : C) (X✝ : D) :
                            (((actionAssocNatIso C D).inv.app X).app X✝).app X✝ = (actionAssocIso X X✝ X✝).inv
                            source
                            def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] :
                            actionLeft D (tensorUnit C) ≅ Functor.id D

                            Bundle λₗ _ as an isomorphism of functors.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_inv_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (X : D) :
                              (actionUnitNatIso C D).inv.app X = (actionUnitIso X).inv
                              source
                              @[simp]
                              theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_hom_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (X : D) :
                              (actionUnitNatIso C D).hom.app X = (actionUnitIso X).hom