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 D
from 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.
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.