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.

We construct similar actions for Cᵒᵖ, namely, left/right Cᵒᵖ-actions on Dᵒᵖ from left/right-actions of C on D, and vice-versa.

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

• One or more equations did not get rendered due to their size.

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_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.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

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

• One or more equations did not get rendered due to their size.

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_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_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_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_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_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.MonoidalLeftAction.oppositeLeftAction (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] : MonoidalLeftAction Cᵒᵖ Dᵒᵖ

Define a left action of Cᵒᵖ on Dᵒᵖ from a left action of C on D via the formula (op c) ⊙ₗ (op d) = op (c ⊙ₗ d).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_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] (c : Cᵒᵖ) (d : Dᵒᵖ) : actionObj c d = Opposite.op (actionObj (Opposite.unop c) (Opposite.unop d))

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_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] {c✝ c'✝ : Cᵒᵖ} (f : c✝ ⟶ c'✝) (d : Dᵒᵖ) : actionHomLeft f d = (actionHomLeft f.unop (Opposite.unop d)).op

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_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 : c✝ ⟶ c'✝) (g : d✝ ⟶ d'✝) : actionHom f g = (actionHom f.unop g.unop).op

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_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] (c : Cᵒᵖ) (x✝ x✝¹ : Dᵒᵖ) (f : x✝ ⟶ x✝¹) : actionHomRight c f = (actionHomRight (Opposite.unop c) f.unop).op

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_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✝ = (actionUnitIso (Opposite.unop x✝)).symm.op

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_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✝ x✝¹ : Cᵒᵖ) (x✝² : Dᵒᵖ) : actionAssocIso x✝ x✝¹ x✝² = (actionAssocIso (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²)).symm.op

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction (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ᵒᵖ] : MonoidalLeftAction C D

Define a left action of C on D from a left action of Cᵒᵖ on Dᵒᵖ via the formula c ⊙ₗ d = unop ((op c) ⊙ₗ (op d)).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_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✝ x✝¹ : C) (x✝² : D) : actionAssocIso x✝ x✝¹ x✝² = (actionAssocIso (Opposite.op x✝) (Opposite.op x✝¹) (Opposite.op x✝²)).symm.unop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_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ᵒᵖ] (c : C) {d d' : D} (f : d ⟶ d') : actionHomRight c f = (actionHomRight (Opposite.op c) f.op).unop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_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 : c ⟶ c') (g : d ⟶ d✝) : actionHom f g = (actionHom f.op g.op).unop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_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ᵒᵖ] {c c' : C} (f : c ⟶ c') (d : D) : actionHomLeft f d = (actionHomLeft f.op (Opposite.op d)).unop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_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ᵒᵖ] (c : C) (d : D) : actionObj c d = Opposite.unop (actionObj (Opposite.op c) (Opposite.op d))

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_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✝ = (actionUnitIso (Opposite.op x✝)).symm.unop

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionObj_op (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 (Opposite.op c) (Opposite.op d) = Opposite.op (actionObj c d)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft_op (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) : actionHomLeft f.op (Opposite.op d) = Opposite.op (actionHomLeft f d)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionRight_op (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') : actionHomRight (Opposite.op c) f.op = Opposite.op (actionHomRight c f)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom_op (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 : c ⟶ c') (g : d ⟶ d') : actionHom f.op g.op = Opposite.op (actionHom f g)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso_op (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 (Opposite.op c) (Opposite.op c') (Opposite.op d) = (actionAssocIso c c' d).symm.op

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionObj_unop (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 (Opposite.unop c) (Opposite.unop d) = Opposite.unop (actionObj c d)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft_unop (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ᵒᵖ) : actionHomLeft f.unop (Opposite.unop d) = Opposite.unop (actionHomLeft f d)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionRight_unop (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') : actionHomRight (Opposite.unop c) f.unop = Opposite.unop (actionHomRight c f)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom_unop (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 : c ⟶ c') (g : d ⟶ d') : actionHom f.unop g.unop = Opposite.unop (actionHom f g)

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso_unop (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 (Opposite.unop c) (Opposite.unop c') (Opposite.unop d) = (actionAssocIso c c' d).symm.unop

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

• One or more equations did not get rendered due to their size.

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_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_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_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

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

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

• One or more equations did not get rendered due to their size.

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_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_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_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_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_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_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

def CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction (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] : MonoidalRightAction Cᵒᵖ Dᵒᵖ

Define a right action of Cᵒᵖ on Dᵒᵖ from a right action of C on D via the formula (op d) ⊙ᵣ (op c) = op (d ⊙ᵣ c).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_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' : Dᵒᵖ} (f : c ⟶ c') (d : Cᵒᵖ) : actionHomLeft f d = (actionHomLeft f.unop (Opposite.unop d)).op

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_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 : d ⟶ d') (g : c ⟶ c') : actionHom f g = (actionHom f.unop g.unop).op

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_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 : Dᵒᵖ) {d d' : Cᵒᵖ} (f : d ⟶ d') : actionHomRight c f = (actionHomRight (Opposite.unop c) f.unop).op

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_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✝ : Dᵒᵖ) (x✝¹ x✝² : Cᵒᵖ) : actionAssocIso x✝ x✝¹ x✝² = (actionAssocIso (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²)).symm.op

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_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 : Dᵒᵖ) (d : Cᵒᵖ) : actionObj c d = Opposite.op (actionObj (Opposite.unop c) (Opposite.unop d))

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_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✝ = (actionUnitIso (Opposite.unop x✝)).symm.op

def CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction (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ᵒᵖ] : MonoidalRightAction C D

Define a right action of C on D from a right action of Cᵒᵖ on Dᵒᵖ via the formula d ⊙ᵣ c = unop ((op d) ⊙ᵣ (op c)).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_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 : D) {d d' : C} (f : d ⟶ d') : actionHomRight c f = (actionHomRight (Opposite.op c) f.op).unop

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_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✝ : D) (x✝¹ x✝² : C) : actionAssocIso x✝ x✝¹ x✝² = (actionAssocIso (Opposite.op x✝) (Opposite.op x✝¹) (Opposite.op x✝²)).symm.unop

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_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' : D} (f : c ⟶ c') (d : C) : actionHomLeft f d = (actionHomLeft f.op (Opposite.op d)).unop

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_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 : d ⟶ d✝) (g : c ⟶ c') : actionHom f g = (actionHom f.op g.op).unop

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_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 : D) (d : C) : actionObj c d = Opposite.unop (actionObj (Opposite.op c) (Opposite.op d))

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_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✝ = (actionUnitIso (Opposite.op x✝)).symm.unop

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionObj_op (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] (d : D) (c : C) : actionObj (Opposite.op d) (Opposite.op c) = Opposite.op (actionObj d c)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft_op (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] {d d' : D} (f : d ⟶ d') (c : C) : actionHomLeft f.op (Opposite.op c) = Opposite.op (actionHomLeft f c)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionRight_op (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] (d : D) {c c' : C} (f : c ⟶ c') : actionHomRight (Opposite.op d) f.op = Opposite.op (actionHomRight d f)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom_op (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] {d d' : D} {c c' : C} (f : d ⟶ d') (g : c ⟶ c') : actionHom f.op g.op = Opposite.op (actionHom f g)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso_op (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] (d : D) (c c' : C) : actionAssocIso (Opposite.op d) (Opposite.op c) (Opposite.op c') = (actionAssocIso d c c').symm.op

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionObj_unop (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ᵒᵖ] (d : Dᵒᵖ) (c : Cᵒᵖ) : actionObj (Opposite.unop d) (Opposite.unop c) = Opposite.unop (actionObj d c)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft_unop (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ᵒᵖ] {d d' : Dᵒᵖ} (f : d ⟶ d') (c : Cᵒᵖ) : actionHomLeft f.unop (Opposite.unop c) = Opposite.unop (actionHomLeft f c)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionRight_unop (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ᵒᵖ] (d : Dᵒᵖ) {c c' : Cᵒᵖ} (f : c ⟶ c') : actionHomRight (Opposite.unop d) f.unop = Opposite.unop (actionHomRight d f)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom_unop (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ᵒᵖ] {d d' : Dᵒᵖ} {c c' : Cᵒᵖ} (f : d ⟶ d') (g : c ⟶ c') : actionHom f.unop g.unop = Opposite.unop (actionHom f g)

theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso_unop (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ᵒᵖ] (d : Dᵒᵖ) (c c' : Cᵒᵖ) : actionAssocIso (Opposite.unop d) (Opposite.unop c) (Opposite.unop c') = (actionAssocIso d c c').symm.unop