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.

We also define right actions, for these, the notation for the action of c on d is d ⊙ᵣ c, and the structure isomorphisms are of the form - ⊙ᵣ (- ⊗ -) ≅ (- ⊙ᵣ -) ⊙ᵣ - and - ⊙ₗ 𝟙_ C ≅ -.

References

• [Janelidze, G, and Kelly, G.M., A note on actions of a monoidal category][JanelidzeKelly2001]

TODOs/Projects

• Equivalence between actions of C on D and pseudofunctors from the classifying bicategory of C to Cat.
• Left/Right Modules in D over a monoid object in C. Equivalence with Mod_ when D is C. Bimodules objects.
• Given a monad M on C, equivalence between Algebra M, and modules in C on M.toMon : Mon (C ⥤ C).
• Canonical left action of Type u on u-small cocomplete categories via the copower.

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

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.

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

Notation for actionObj, the action of C on D.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊵ₗ_» : Lean.TrailingParserDescr

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

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊴ₗ_» : Lean.TrailingParserDescr

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

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

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

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.termαₗ : Lean.ParserDescr

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

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.«termλₗ» : Lean.ParserDescr

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

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

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

class CategoryTheory.MonoidalCategory.MonoidalLeftAction (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] extends CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D : Type (max (max (max u_1 u_2) v_1) v_2)

A MonoidalLeftAction C D 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 compatibilities with the associator and unitor isomorphisms in C.

• actionObj : C → D → D
• actionHomLeft {c c' : C} (f : c ⟶ c') (d : D) : actionObj c d ⟶ actionObj c' d
• actionHomRight (c : C) {d d' : D} (f : d ⟶ d') : actionObj c d ⟶ actionObj c d'
• actionHom {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d') : actionObj c d ⟶ actionObj c' d'
• actionAssocIso (c c' : C) (d : D) : actionObj (tensorObj c c') d ≅ actionObj c (actionObj c' d)
• actionUnitIso (d : D) : actionObj (tensorUnit C) d ≅ d
• actionHom_def {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d') : actionHom f g = CategoryStruct.comp (actionHomLeft f d) (actionHomRight c' g)
• actionHomRight_id (c : C) (d : D) : actionHomRight c (CategoryStruct.id d) = CategoryStruct.id (actionObj c d)
• id_actionHomLeft (c : C) (d : D) : actionHomLeft (CategoryStruct.id c) d = CategoryStruct.id (actionObj c d)
• actionHom_comp {c c' c'' : C} {d d' d'' : D} (f₁ : c ⟶ c') (f₂ : c' ⟶ c'') (g₁ : d ⟶ d') (g₂ : d' ⟶ d'') : actionHom (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂) = CategoryStruct.comp (actionHom f₁ g₁) (actionHom f₂ g₂)
• actionAssocIso_hom_naturality {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂) (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂) : CategoryStruct.comp (actionHom (tensorHom f g) h) (actionAssocIso c₂ c₄ d₂).hom = CategoryStruct.comp (actionAssocIso c₁ c₃ d₁).hom (actionHom f (actionHom g h))
• actionUnitIso_hom_naturality {d d' : D} (f : d ⟶ d') : CategoryStruct.comp (actionUnitIso d).hom f = CategoryStruct.comp (actionHomRight (tensorUnit C) f) (actionUnitIso d').hom
• whiskerLeft_actionHomLeft (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D) : actionHomLeft (whiskerLeft c f) d = CategoryStruct.comp (actionAssocIso c c' d).hom (CategoryStruct.comp (actionHomRight c (actionHomLeft f d)) (actionAssocIso c c'' d).inv)
• whiskerRight_actionHomLeft {c c' : C} (c'' : C) (f : c ⟶ c') (d : D) : actionHomLeft (whiskerRight f c'') d = CategoryStruct.comp (actionAssocIso c c'' d).hom (CategoryStruct.comp (actionHomLeft f (actionObj c'' d)) (actionAssocIso c' c'' d).inv)
• associator_actionHom (c₁ c₂ c₃ : C) (d : D) : CategoryStruct.comp (actionHomLeft (associator c₁ c₂ c₃).hom d) (CategoryStruct.comp (actionAssocIso c₁ (tensorObj c₂ c₃) d).hom (actionHomRight c₁ (actionAssocIso c₂ c₃ d).hom)) = CategoryStruct.comp (actionAssocIso (tensorObj c₁ c₂) c₃ d).hom (actionAssocIso c₁ c₂ (actionObj c₃ d)).hom
• leftUnitor_actionHom (c : C) (d : D) : actionHomLeft (leftUnitor c).hom d = CategoryStruct.comp (actionAssocIso (tensorUnit C) c d).hom (actionUnitIso (actionObj c d)).hom
• rightUnitor_actionHom (c : C) (d : D) : actionHomLeft (rightUnitor c).hom d = CategoryStruct.comp (actionAssocIso c (tensorUnit C) d).hom (actionHomRight c (actionUnitIso d).hom)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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))

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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✝)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, 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)

instance CategoryTheory.MonoidalCategory.selfLeftAction (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] : MonoidalLeftAction C C

A monoidal category acts on itself on the left through the tensor product.

@[simp]

theorem CategoryTheory.MonoidalCategory.selfLeftAction_actionAssocIso (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x y z : C) : MonoidalLeftActionStruct.actionAssocIso x y z = associator x y z

@[simp]

theorem CategoryTheory.MonoidalCategory.selfLeftAction_actionObj (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x y : C) : MonoidalLeftActionStruct.actionObj x y = tensorObj x y

@[simp]

theorem CategoryTheory.MonoidalCategory.selfLeftAction_actionHomRight (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x x✝ x✝¹ : C) (f : x✝ ⟶ x✝¹) : MonoidalLeftActionStruct.actionHomRight x f = whiskerLeft x f

@[simp]

theorem CategoryTheory.MonoidalCategory.selfLeftAction_actionUnitIso (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x : C) : MonoidalLeftActionStruct.actionUnitIso x = leftUnitor x

@[simp]

theorem CategoryTheory.MonoidalCategory.selfLeftAction_actionHom (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] {c✝ c'✝ d✝ d'✝ : C} (f : c✝ ⟶ c'✝) (g : d✝ ⟶ d'✝) : MonoidalLeftActionStruct.actionHom f g = tensorHom f g

@[simp]

theorem CategoryTheory.MonoidalCategory.selfLeftAction_actionHomLeft (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] {c✝ c'✝ : C} (f : c✝ ⟶ c'✝) (x : C) : MonoidalLeftActionStruct.actionHomLeft f x = whiskerRight f x

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (c : C) {d d' : D} (f : d ⟶ d') : actionHom (CategoryStruct.id c) f = actionHomRight c f

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {c c' : C} (f : c ⟶ c') (d : D) : actionHom f (CategoryStruct.id d) = actionHomLeft f d

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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))

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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))

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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))

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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₂)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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✝)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z) [IsIso f] : IsIso (actionHomRight x f)

instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] {x y : C} (f : x ⟶ y) [IsIso f] (z : D) : IsIso (actionHomLeft f z)

instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, 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.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_map_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_obj_obj (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (x : C) (y : D) : ((curriedAction C D).obj x).obj y = actionObj x y

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_obj_map (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, 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

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft {C : Type u_1} (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (c : C) : Functor D D

Bundle d ↦ c ⊙ₗ d as a functor.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft_map {C : Type u_1} (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (c : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (actionLeft D c).map f = actionHomRight c f

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft_obj {C : Type u_1} (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (c : C) (y : D) : (actionLeft D c).obj y = actionObj c y

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight (C : Type u_1) {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (d : D) : Functor C D

Bundle c ↦ c ⊙ₗ d as a functor.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight_map (C : Type u_1) {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (d : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (actionRight C d).map f = actionHomLeft f d

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight_obj (C : Type u_1) {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (d : D) (j : C) : (actionRight C d).obj j = actionObj j d

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, 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.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_hom_app_app_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, 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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_inv_app_app_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, 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

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] : actionLeft D (tensorUnit C) ≅ Functor.id D

Bundle λₗ _ as an isomorphism of functors.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_hom_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (X : D) : (actionUnitNatIso C D).hom.app X = (actionUnitIso X).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_inv_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalLeftAction C D] (X : D) : (actionUnitNatIso C D).inv.app X = (actionUnitIso X).inv

class CategoryTheory.MonoidalCategory.MonoidalRightActionStruct (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategoryStruct C] : Type (max (max (max u_1 u_2) v_1) v_2)

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

• actionObj : D → C → D

  The right action on objects. This is denoted d ⊙ᵣ c.

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

  The right 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 d ⊴ᵣ f.

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

  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 f ⊵ᵣ c.

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

  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 (d : D) (c c' : C) : actionObj d (tensorObj c c') ≅ actionObj (actionObj d c) c'

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

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

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

def CategoryTheory.MonoidalCategory.MonoidalRightAction.«term_⊙ᵣ_» : Lean.TrailingParserDescr

Notation for actionObj, the action of C on D.

def CategoryTheory.MonoidalCategory.MonoidalRightAction.«term_⊵ᵣ_» : Lean.TrailingParserDescr

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

def CategoryTheory.MonoidalCategory.MonoidalRightAction.«term_⊴ᵣ_» : Lean.TrailingParserDescr

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

def CategoryTheory.MonoidalCategory.MonoidalRightAction.«term_⊙ᵣₘ_» : Lean.TrailingParserDescr

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

def CategoryTheory.MonoidalCategory.MonoidalRightAction.termαᵣ : Lean.ParserDescr

Notation for actionAssocIso, the structural isomorphism - ⊙ᵣ (- ⊗ -) ≅ (- ⊙ᵣ -) ⊙ᵣ -.

def CategoryTheory.MonoidalCategory.MonoidalRightAction.termρᵣ : Lean.ParserDescr

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

def CategoryTheory.MonoidalCategory.MonoidalRightAction.«termρᵣ[_]» : Lean.ParserDescr

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

class CategoryTheory.MonoidalCategory.MonoidalRightAction (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] extends CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D : Type (max (max (max u_1 u_2) v_1) v_2)

A MonoidalRightAction C D 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 compatibilities with the associator and unitor isomorphisms in C.

• actionObj : D → C → D
• actionHomRight (d : D) {c c' : C} (f : c ⟶ c') : actionObj d c ⟶ actionObj d c'
• actionHomLeft {d d' : D} (f : d ⟶ d') (c : C) : actionObj d c ⟶ actionObj d' c
• actionHom {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c') : actionObj d c ⟶ actionObj d' c'
• actionAssocIso (d : D) (c c' : C) : actionObj d (tensorObj c c') ≅ actionObj (actionObj d c) c'
• actionUnitIso (d : D) : actionObj d (tensorUnit C) ≅ d
• actionHom_def {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c') : actionHom f g = CategoryStruct.comp (actionHomLeft f c) (actionHomRight d' g)
• actionHomRight_id (c : C) (d : D) : actionHomRight d (CategoryStruct.id c) = CategoryStruct.id (actionObj d c)
• id_actionHomLeft (c : C) (d : D) : actionHomLeft (CategoryStruct.id d) c = CategoryStruct.id (actionObj d c)
• actionHom_comp {c c' c'' : C} {d d' d'' : D} (f₁ : d ⟶ d') (f₂ : d' ⟶ d'') (g₁ : c ⟶ c') (g₂ : c' ⟶ c'') : actionHom (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂) = CategoryStruct.comp (actionHom f₁ g₁) (actionHom f₂ g₂)
• actionAssocIso_hom_naturality {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂) (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄) : CategoryStruct.comp (actionHom f (tensorHom g h)) (actionAssocIso d₂ c₂ c₄).hom = CategoryStruct.comp (actionAssocIso d₁ c₁ c₃).hom (actionHom (actionHom f g) h)
• actionUnitIso_hom_naturality {d d' : D} (f : d ⟶ d') : CategoryStruct.comp (actionUnitIso d).hom f = CategoryStruct.comp (actionHomLeft f (tensorUnit C)) (actionUnitIso d').hom
• actionHomRight_whiskerRight {c' c'' : C} (f : c' ⟶ c'') (c : C) (d : D) : actionHomRight d (whiskerRight f c) = CategoryStruct.comp (actionAssocIso d c' c).hom (CategoryStruct.comp (actionHomLeft (actionHomRight d f) c) (actionAssocIso d c'' c).inv)
• whiskerRight_actionHomLeft (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D) : actionHomRight d (whiskerLeft c f) = CategoryStruct.comp (actionAssocIso d c c').hom (CategoryStruct.comp (actionHomRight (actionObj d c) f) (actionAssocIso d c c'').inv)
• actionHom_associator (c₁ c₂ c₃ : C) (d : D) : CategoryStruct.comp (actionHomRight d (associator c₁ c₂ c₃).hom) (CategoryStruct.comp (actionAssocIso d c₁ (tensorObj c₂ c₃)).hom (actionAssocIso (actionObj d c₁) c₂ c₃).hom) = CategoryStruct.comp (actionAssocIso d (tensorObj c₁ c₂) c₃).hom (actionHomLeft (actionAssocIso d c₁ c₂).hom c₃)
• actionHom_leftUnitor (c : C) (d : D) : actionHomRight d (leftUnitor c).hom = CategoryStruct.comp (actionAssocIso d (tensorUnit C) c).hom (actionHomLeft (actionUnitIso d).hom c)
• actionHom_rightUnitor (c : C) (d : D) : actionHomRight d (rightUnitor c).hom = CategoryStruct.comp (actionAssocIso d c (tensorUnit C)).hom (actionUnitIso (actionObj d c)).hom

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c') {Z : D} (h : actionObj d' c' ⟶ Z) : CategoryStruct.comp (actionHom f g) h = CategoryStruct.comp (actionHomLeft f c) (CategoryStruct.comp (actionHomRight d' g) h)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] (c : C) (d : D) {Z : D} (h : actionObj d c ⟶ Z) : CategoryStruct.comp (actionHomLeft (CategoryStruct.id d) c) h = h

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] (c : C) (d : D) {Z : D} (h : actionObj d c ⟶ Z) : CategoryStruct.comp (actionHomRight d (CategoryStruct.id c)) h = h

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] {c' c'' : C} (f : c' ⟶ c'') (c : C) (d : D) {Z : D} (h : actionObj d (tensorObj c'' c) ⟶ Z) : CategoryStruct.comp (actionHomRight d (whiskerRight f c)) h = CategoryStruct.comp (actionAssocIso d c' c).hom (CategoryStruct.comp (actionHomLeft (actionHomRight d f) c) (CategoryStruct.comp (actionAssocIso d c'' c).inv h))

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] {c c' c'' : C} {d d' d'' : D} (f₁ : d ⟶ d') (f₂ : d' ⟶ d'') (g₁ : c ⟶ c') (g₂ : c' ⟶ c'') {Z : D} (h : actionObj d'' c'' ⟶ Z) : CategoryStruct.comp (actionHom (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂)) h = CategoryStruct.comp (actionHom f₁ g₁) (CategoryStruct.comp (actionHom f₂ g₂) h)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂) (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄) {Z : D} (h✝ : actionObj (actionObj d₂ c₂) c₄ ⟶ Z) : CategoryStruct.comp (actionHom f (tensorHom g h)) (CategoryStruct.comp (actionAssocIso d₂ c₂ c₄).hom h✝) = CategoryStruct.comp (actionAssocIso d₁ c₁ c₃).hom (CategoryStruct.comp (actionHom (actionHom f g) h) h✝)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] {d d' : D} (f : d ⟶ d') {Z : D} (h : d' ⟶ Z) : CategoryStruct.comp (actionUnitIso d).hom (CategoryStruct.comp f h) = CategoryStruct.comp (actionHomLeft f (tensorUnit C)) (CategoryStruct.comp (actionUnitIso d').hom h)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] (c₁ c₂ c₃ : C) (d : D) {Z : D} (h : actionObj (actionObj (actionObj d c₁) c₂) c₃ ⟶ Z) : CategoryStruct.comp (actionHomRight d (associator c₁ c₂ c₃).hom) (CategoryStruct.comp (actionAssocIso d c₁ (tensorObj c₂ c₃)).hom (CategoryStruct.comp (actionAssocIso (actionObj d c₁) c₂ c₃).hom h)) = CategoryStruct.comp (actionAssocIso d (tensorObj c₁ c₂) c₃).hom (CategoryStruct.comp (actionHomLeft (actionAssocIso d c₁ c₂).hom c₃) h)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] (c : C) (d : D) {Z : D} (h : actionObj d c ⟶ Z) : CategoryStruct.comp (actionHomRight d (leftUnitor c).hom) h = CategoryStruct.comp (actionAssocIso d (tensorUnit C) c).hom (CategoryStruct.comp (actionHomLeft (actionUnitIso d).hom c) h)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor_assoc {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {inst✝² : MonoidalCategory C} [self : MonoidalRightAction C D] (c : C) (d : D) {Z : D} (h : actionObj d c ⟶ Z) : CategoryStruct.comp (actionHomRight d (rightUnitor c).hom) h = CategoryStruct.comp (actionAssocIso d c (tensorUnit C)).hom (CategoryStruct.comp (actionUnitIso (actionObj d c)).hom h)

instance CategoryTheory.MonoidalCategory.selRightfAction (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] : MonoidalRightAction C C

A monoidal category acts on itself through the tensor product.

@[simp]

theorem CategoryTheory.MonoidalCategory.selRightfAction_actionHom (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] {c✝ c'✝ d✝ d'✝ : C} (f : d✝ ⟶ d'✝) (g : c✝ ⟶ c'✝) : MonoidalRightActionStruct.actionHom f g = tensorHom f g

@[simp]

theorem CategoryTheory.MonoidalCategory.selRightfAction_actionHomRight (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x x✝ x✝¹ : C) (f : x✝ ⟶ x✝¹) : MonoidalRightActionStruct.actionHomRight x f = whiskerLeft x f

@[simp]

theorem CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_hom (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x y z : C) : (MonoidalRightActionStruct.actionAssocIso x y z).hom = (associator x y z).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_inv (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x y z : C) : (MonoidalRightActionStruct.actionAssocIso x y z).inv = (associator x y z).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.selRightfAction_actionUnitIso (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x : C) : MonoidalRightActionStruct.actionUnitIso x = rightUnitor x

@[simp]

theorem CategoryTheory.MonoidalCategory.selRightfAction_actionHomLeft (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] {d✝ d'✝ : C} (f : d✝ ⟶ d'✝) (x : C) : MonoidalRightActionStruct.actionHomLeft f x = whiskerRight f x

@[simp]

theorem CategoryTheory.MonoidalCategory.selRightfAction_actionObj (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (x y : C) : MonoidalRightActionStruct.actionObj x y = tensorObj x y

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {d d' : D} (f : d ⟶ d') (c : C) : actionHom f (CategoryStruct.id c) = actionHomLeft f c

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (d : D) {c c' : C} (f : c ⟶ c') : actionHom (CategoryStruct.id d) f = actionHomRight d f

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (w : D) {x y z : C} (f : x ⟶ y) (g : y ⟶ z) : actionHomRight w (CategoryStruct.comp f g) = CategoryStruct.comp (actionHomRight w f) (actionHomRight w g)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (w : D) {x y z : C} (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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ⟶ y) : actionHomLeft f (tensorUnit C) = CategoryStruct.comp (actionUnitIso x).hom (CategoryStruct.comp f (actionUnitIso y).inv)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ⟶ y) {Z : D} (h : actionObj y (tensorUnit C) ⟶ Z) : CategoryStruct.comp (actionHomLeft f (tensorUnit C)) h = CategoryStruct.comp (actionUnitIso x).hom (CategoryStruct.comp f (CategoryStruct.comp (actionUnitIso y).inv h))

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {z z' : D} (f : z ⟶ z') (x y : C) : actionHomLeft f (tensorObj x y) = CategoryStruct.comp (actionAssocIso z x y).hom (CategoryStruct.comp (actionHomLeft (actionHomLeft f x) y) (actionAssocIso z' x y).inv)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {z z' : D} (f : z ⟶ z') (x y : C) {Z : D} (h : actionObj z' (tensorObj x y) ⟶ Z) : CategoryStruct.comp (actionHomLeft f (tensorObj x y)) h = CategoryStruct.comp (actionAssocIso z x y).hom (CategoryStruct.comp (actionHomLeft (actionHomLeft f x) y) (CategoryStruct.comp (actionAssocIso z' x y).inv h))

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {w x y : D} (f : w ⟶ x) (g : x ⟶ y) (z : C) : actionHomLeft (CategoryStruct.comp f g) z = CategoryStruct.comp (actionHomLeft f z) (actionHomLeft g z)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {w x y : D} (f : w ⟶ x) (g : x ⟶ y) (z : C) {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)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (y : D) (z : C) {x x' : C} (f : x ⟶ x') : actionHomRight (actionObj y z) f = CategoryStruct.comp (actionAssocIso y z x).inv (CategoryStruct.comp (actionHomRight y (whiskerLeft z f)) (actionAssocIso y z x').hom)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (y : D) (z : C) {x x' : C} (f : x ⟶ x') {Z : D} (h : actionObj (actionObj y z) x' ⟶ Z) : CategoryStruct.comp (actionHomRight (actionObj y z) f) h = CategoryStruct.comp (actionAssocIso y z x).inv (CategoryStruct.comp (actionHomRight y (whiskerLeft z f)) (CategoryStruct.comp (actionAssocIso y z x').hom h))

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {w x : D} {y z : C} (f : w ⟶ x) (g : y ⟶ z) : CategoryStruct.comp (actionHomRight w g) (actionHomLeft f z) = CategoryStruct.comp (actionHomLeft f y) (actionHomRight x g)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {w x : D} {y z : C} (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)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x₁ y₁ : D} {x₂ y₂ : C} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂) : actionHom f g = CategoryStruct.comp (actionHomRight x₁ g) (actionHomLeft f y₂)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x₁ y₁ : D} {x₂ y₂ : C} (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)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂) (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄) : CategoryStruct.comp (actionHom (actionHom f g) h) (actionAssocIso d₂ c₂ c₄).inv = CategoryStruct.comp (actionAssocIso d₁ c₁ c₃).inv (actionHom f (tensorHom g h))

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂) (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄) {Z : D} (h✝ : actionObj d₂ (tensorObj c₂ c₄) ⟶ Z) : CategoryStruct.comp (actionHom (actionHom f g) h) (CategoryStruct.comp (actionAssocIso d₂ c₂ c₄).inv h✝) = CategoryStruct.comp (actionAssocIso d₁ c₁ c₃).inv (CategoryStruct.comp (actionHom f (tensorHom g h)) h✝)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {d d' : D} (f : d ⟶ d') : CategoryStruct.comp (actionUnitIso d).inv (actionHomLeft f (tensorUnit C)) = CategoryStruct.comp f (actionUnitIso d').inv

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {d d' : D} (f : d ⟶ d') {Z : D} (h : actionObj d' (tensorUnit C) ⟶ Z) : CategoryStruct.comp (actionUnitIso d).inv (CategoryStruct.comp (actionHomLeft f (tensorUnit C)) h) = CategoryStruct.comp f (CategoryStruct.comp (actionUnitIso d').inv h)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (f : y ≅ z) : CategoryStruct.comp (actionHomRight x f.hom) (actionHomRight x f.inv) = CategoryStruct.id (actionObj x y)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (f : y ≅ z) {Z : D} (h : actionObj x y ⟶ Z) : CategoryStruct.comp (actionHomRight x f.hom) (CategoryStruct.comp (actionHomRight x f.inv) h) = h

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ≅ y) (z : C) : CategoryStruct.comp (actionHomLeft f.hom z) (actionHomLeft f.inv z) = CategoryStruct.id (actionObj x z)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ≅ y) (z : C) {Z : D} (h : actionObj x z ⟶ Z) : CategoryStruct.comp (actionHomLeft f.hom z) (CategoryStruct.comp (actionHomLeft f.inv z) h) = h

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (f : y ≅ z) : CategoryStruct.comp (actionHomRight x f.inv) (actionHomRight x f.hom) = CategoryStruct.id (actionObj x z)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (f : y ≅ z) {Z : D} (h : actionObj x z ⟶ Z) : CategoryStruct.comp (actionHomRight x f.inv) (CategoryStruct.comp (actionHomRight x f.hom) h) = h

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ≅ y) (z : C) : CategoryStruct.comp (actionHomLeft f.inv z) (actionHomLeft f.hom z) = CategoryStruct.id (actionObj y z)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ≅ y) (z : C) {Z : D} (h : actionObj y z ⟶ Z) : CategoryStruct.comp (actionHomLeft f.inv z) (CategoryStruct.comp (actionHomLeft f.hom z) h) = h

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z) [IsIso f] : CategoryStruct.comp (actionHomRight x f) (actionHomRight x (inv f)) = CategoryStruct.id (actionObj x y)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ⟶ y) [IsIso f] (z : C) : CategoryStruct.comp (actionHomLeft f z) (actionHomLeft (inv f) z) = CategoryStruct.id (actionObj x z)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ⟶ y) [IsIso f] (z : C) {Z : D} (h : actionObj x z ⟶ Z) : CategoryStruct.comp (actionHomLeft f z) (CategoryStruct.comp (actionHomLeft (inv f) z) h) = h

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z) [IsIso f] : CategoryStruct.comp (actionHomRight x (inv f)) (actionHomRight x f) = CategoryStruct.id (actionObj x z)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ⟶ y) [IsIso f] (z : C) : CategoryStruct.comp (actionHomLeft (inv f) z) (actionHomLeft f z) = CategoryStruct.id (actionObj y z)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft'_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ⟶ y) [IsIso f] (z : C) {Z : D} (h : actionObj y z ⟶ Z) : CategoryStruct.comp (actionHomLeft (inv f) z) (CategoryStruct.comp (actionHomLeft f z) h) = h

instance CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ⟶ y) [IsIso f] (z : C) : IsIso (actionHomLeft f z)

instance CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z) [IsIso f] : IsIso (actionHomRight x f)

instance CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} {x' y' : C} (f : x ⟶ y) (g : x' ⟶ y') [IsIso f] [IsIso g] : IsIso (actionHom f g)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHomLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} (f : x ⟶ y) [IsIso f] (z : C) : inv (actionHomLeft f z) = actionHomLeft (inv f) z

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHomRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z) [IsIso f] : inv (actionHomRight x f) = actionHomRight x (inv f)

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {x y : D} {x' y' : C} (f : x ⟶ y) (g : x' ⟶ y') [IsIso f] [IsIso g] : inv (actionHom f g) = actionHom (inv f) (inv g)

def CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] : Functor C (Functor D D)

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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_obj_map (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((curriedAction C D).obj x).map f = actionHomLeft f x

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_map_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (y : D) : ((curriedAction C D).map f).app y = actionHomRight y f

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_obj_obj (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (x : C) (y : D) : ((curriedAction C D).obj x).obj y = actionObj y x

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.MonoidalRightAction.actionRight {C : Type u_1} (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (c : C) : Functor D D

Bundle d ↦ d ⊙ᵣ c as a functor.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionRight_map {C : Type u_1} (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (c : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (actionRight D c).map f = actionHomLeft f c

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionRight_obj {C : Type u_1} (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (c : C) (y : D) : (actionRight D c).obj y = actionObj y c

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.MonoidalRightAction.actionLeft (C : Type u_1) {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (d : D) : Functor C D

Bundle c ↦ d ⊙ᵣ c as a functor.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionLeft_obj (C : Type u_1) {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (d : D) (j : C) : (actionLeft C d).obj j = actionObj d j

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionLeft_map (C : Type u_1) {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (d : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (actionLeft C d).map f = actionHomRight d f

def CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] : bifunctorComp₁₂ (curriedTensor C) (curriedAction C D) ≅ (bifunctorComp₂₃ (curriedAction C D) (curriedAction C D)).flip

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

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso_inv_app_app_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (X X✝ : C) (X✝¹ : D) : (((actionAssocNatIso C D).inv.app X).app X✝).app X✝¹ = (actionAssocIso X✝¹ X X✝).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso_hom_app_app_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (X X✝ : C) (X✝¹ : D) : (((actionAssocNatIso C D).hom.app X).app X✝).app X✝¹ = (actionAssocIso X✝¹ X X✝).hom

def CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] : actionRight D (tensorUnit C) ≅ Functor.id D

Bundle ρᵣ _ as an isomorphism of functors.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso_hom_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (X : D) : (actionUnitNatIso C D).hom.app X = (actionUnitIso X).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso_inv_app (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalRightAction C D] (X : D) : (actionUnitNatIso C D).inv.app X = (actionUnitIso X).inv