Documentation

Mathlib.CategoryTheory.Monoidal.Action.Opposites

Actions from the monoidal opposite of a category. #

In this file, given a monoidal category C and a category D, we construct a left C-action on D out of the data of a right Cᴹᵒᵖ-action on D. We also construct a right C-action on Dfrom the data of a left Cᴹᵒᵖ-action on D. Conversely, given left/right C-actions on D, we construct aCᴹᵒᵖ actions with the conjugate variance.

These constructions are not made instances in order to avoid instance loops, you should bring them as local instances if you intend to use them.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction Cᴹᵒᵖ D] :

MonoidalLeftAction C D

Define a left action of C on D from a right action of Cᴹᵒᵖ on D via the formula c ⊙ₗ d := d ⊙ᵣ (mop c).

Equations

Instances For

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction Cᴹᵒᵖ D] {c c' : C} {d d✝ : D} (f : c ⟶ c') (g : d ⟶ d✝) :

actionHom f g = MonoidalRightActionStruct.actionHom g f.mop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionObj (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction Cᴹᵒᵖ D] (c : C) (d : D) :

actionObj c d = MonoidalRightActionStruct.actionObj d { unmop := c }

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomRight (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction Cᴹᵒᵖ D] (c : C) {d d' : D} (f : d ⟶ d') :

actionHomRight c f = MonoidalRightActionStruct.actionHomLeft f { unmop := c }

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionAssocIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction Cᴹᵒᵖ D] (x✝ x✝¹ : C) (x✝² : D) :

actionAssocIso x✝ x✝¹ x✝² = MonoidalRightActionStruct.actionAssocIso x✝² { unmop := x✝¹ } { unmop := x✝ }

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction Cᴹᵒᵖ D] {c c' : C} (f : c ⟶ c') (d : D) :

actionHomLeft f d = MonoidalRightActionStruct.actionHomRight d f.mop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionUnitIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction Cᴹᵒᵖ D] (x✝ : D) :

actionUnitIso x✝ = MonoidalRightActionStruct.actionUnitIso x✝

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] :

MonoidalLeftAction Cᴹᵒᵖ D

Define a left action of Cᴹᵒᵖ on D from a right action of C on D via the formula mop c ⊙ₗ d = d ⊙ᵣ c.

Equations

Instances For

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] {c c' : Cᴹᵒᵖ} {d d✝ : D} (f : c ⟶ c') (g : d ⟶ d✝) :

actionHom f g = MonoidalRightActionStruct.actionHom g f.unmop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionUnitIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] (x✝ : D) :

actionUnitIso x✝ = MonoidalRightActionStruct.actionUnitIso x✝

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] (c : Cᴹᵒᵖ) {d d' : D} (f : d ⟶ d') :

actionHomRight c f = MonoidalRightActionStruct.actionHomLeft f c.unmop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] (c : Cᴹᵒᵖ) (d : D) :

actionObj c d = MonoidalRightActionStruct.actionObj d c.unmop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] {c c' : Cᴹᵒᵖ} (f : c ⟶ c') (d : D) :

actionHomLeft f d = MonoidalRightActionStruct.actionHomRight d f.unmop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] (x✝ x✝¹ : Cᴹᵒᵖ) (x✝² : D) :

actionAssocIso x✝ x✝¹ x✝² = MonoidalRightActionStruct.actionAssocIso x✝² x✝¹.unmop x✝.unmop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] (c : C) (d : D) :

actionObj { unmop := c } d = MonoidalRightActionStruct.actionObj d c

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] {c c' : C} (f : c ⟶ c') (d : D) :

actionHomLeft f.mop d = MonoidalRightActionStruct.actionHomRight d f

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [MonoidalCategory C] [Category.{u_3, u_2} D] [MonoidalRightAction C D] (c : C) {d d' : D} (f : d ⟶ d') :

actionHomRight { unmop := c } f = MonoidalRightActionStruct.actionHomLeft f c

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalRightAction C D] {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d') :

actionHom f.mop g = MonoidalRightActionStruct.actionHom g f

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [MonoidalCategory C] [Category.{u_3, u_2} D] [MonoidalRightAction C D] (c c' : C) (d : D) :

actionAssocIso { unmop := c } { unmop := c' } d = MonoidalRightActionStruct.actionAssocIso d c' c

def CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction Cᴹᵒᵖ D] :

MonoidalRightAction C D

Define a right action of C on D from a left action of Cᴹᵒᵖ on D via the formula d ⊙ᵣ c := (mop c) ⊙ₗ d.

Equations

Instances For

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomLeft (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction Cᴹᵒᵖ D] {d d' : D} (f : d ⟶ d') (c : C) :

actionHomLeft f c = MonoidalLeftActionStruct.actionHomRight { unmop := c } f

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionObj (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction Cᴹᵒᵖ D] (d : D) (c : C) :

actionObj d c = MonoidalLeftActionStruct.actionObj { unmop := c } d

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction Cᴹᵒᵖ D] (d : D) (x✝ x✝¹ : C) (f : x✝ ⟶ x✝¹) :

actionHomRight d f = MonoidalLeftActionStruct.actionHomLeft f.mop d

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionAssocIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction Cᴹᵒᵖ D] (x✝ : D) (x✝¹ x✝² : C) :

actionAssocIso x✝ x✝¹ x✝² = MonoidalLeftActionStruct.actionAssocIso { unmop := x✝² } { unmop := x✝¹ } x✝

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionUnitIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction Cᴹᵒᵖ D] (x✝ : D) :

actionUnitIso x✝ = MonoidalLeftActionStruct.actionUnitIso x✝

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction Cᴹᵒᵖ D] {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c') :

actionHom f g = MonoidalLeftActionStruct.actionHom g.mop f

def CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] :

MonoidalRightAction Cᴹᵒᵖ D

Define a right action of Cᴹᵒᵖ on D from a left action of C on D via the formula d ⊙ᵣ mop c = c ⊙ₗ d.

Equations

Instances For

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] (d : D) (x✝ x✝¹ : Cᴹᵒᵖ) (f : x✝ ⟶ x✝¹) :

actionHomRight d f = MonoidalLeftActionStruct.actionHomLeft f.unmop d

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] (x✝ : D) (x✝¹ x✝² : Cᴹᵒᵖ) :

actionAssocIso x✝ x✝¹ x✝² = MonoidalLeftActionStruct.actionAssocIso x✝².unmop x✝¹.unmop x✝

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionUnitIso (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] (x✝ : D) :

actionUnitIso x✝ = MonoidalLeftActionStruct.actionUnitIso x✝

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] {d d' : D} (f : d ⟶ d') (c : Cᴹᵒᵖ) :

actionHomLeft f c = MonoidalLeftActionStruct.actionHomRight c.unmop f

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] (d : D) (c : Cᴹᵒᵖ) :

actionObj d c = MonoidalLeftActionStruct.actionObj c.unmop d

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] {c c' : Cᴹᵒᵖ} {d d' : D} (f : d ⟶ d') (g : c ⟶ c') :

actionHom f g = MonoidalLeftActionStruct.actionHom g.unmop f

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] (c : C) (d : D) :

actionObj d { unmop := c } = MonoidalLeftActionStruct.actionObj c d

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [MonoidalCategory C] [Category.{u_4, u_2} D] [MonoidalLeftAction C D] {c c' : C} (f : c ⟶ c') (d : D) :

actionHomRight d f.mop = MonoidalLeftActionStruct.actionHomLeft f d

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionRight_mop (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [MonoidalCategory C] [Category.{u_3, u_2} D] [MonoidalLeftAction C D] (c : C) {d d' : D} (f : d ⟶ d') :

actionHomLeft f { unmop := c } = MonoidalLeftActionStruct.actionHomRight c f

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [MonoidalCategory C] [Category.{u_3, u_2} D] [MonoidalLeftAction C D] {c c' : D} {d d' : C} (f : c ⟶ c') (g : d ⟶ d') :

actionHom f g.mop = MonoidalLeftActionStruct.actionHom g f

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [MonoidalCategory C] [Category.{u_3, u_2} D] [MonoidalLeftAction C D] (c c' : C) (d : D) :

actionAssocIso d { unmop := c } { unmop := c' } = MonoidalLeftActionStruct.actionAssocIso c' c d