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.

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