Unit-prefixed associator and braiding values in SuperVect

The category SuperVect — finite-dimensional ℤ/2-graded complex vector spaces with the graded tensor product and the Koszul braiding — is defined, with its monoidal, braided, symmetric, additive and ℂ-linear structure, in RS/Definitions.lean. This module carries the value computations the extraction consumes: the unit-prefixed associator and inverse associator on the four graded blocks, and the braiding on the four generator shapes, including the Koszul sign on odd⊗odd.

Unit-prefixed associator and braiding values

theorem RS.SuperVect.assoc_unit_ee {V : SuperVect} (r : ℂ) (x y : V.even) : (tensorUnit.associator V V).hom.evenMap ((r ⊗ₜ[ℂ] x, 0) ⊗ₜ[ℂ] y, 0) = (r ⊗ₜ[ℂ] (x ⊗ₜ[ℂ] y, 0), 0)

The unit-prefixed associator on the even-even block.

theorem RS.SuperVect.assoc_unit_oo {V : SuperVect} (r : ℂ) (u v : V.odd) : (tensorUnit.associator V V).hom.evenMap (0, (r ⊗ₜ[ℂ] u, 0) ⊗ₜ[ℂ] v) = (r ⊗ₜ[ℂ] (0, u ⊗ₜ[ℂ] v), 0)

The unit-prefixed associator on the odd-odd block.

theorem RS.SuperVect.assoc_unit_eo {V : SuperVect} (r : ℂ) (x : V.even) (v : V.odd) : (tensorUnit.associator V V).hom.oddMap ((r ⊗ₜ[ℂ] x, 0) ⊗ₜ[ℂ] v, 0) = (r ⊗ₜ[ℂ] (x ⊗ₜ[ℂ] v, 0), 0)

The unit-prefixed associator on the even-odd block.

theorem RS.SuperVect.assoc_unit_oe {V : SuperVect} (r : ℂ) (u : V.odd) (y : V.even) : (tensorUnit.associator V V).hom.oddMap (0, (r ⊗ₜ[ℂ] u, 0) ⊗ₜ[ℂ] y) = (r ⊗ₜ[ℂ] (0, u ⊗ₜ[ℂ] y), 0)

The unit-prefixed associator on the odd-even block.

theorem RS.SuperVect.koszul_ee {V W : SuperVect} (x : V.even) (w : W.even) : (V.koszulBraiding W).evenMap (x ⊗ₜ[ℂ] w, 0) = (w ⊗ₜ[ℂ] x, 0)

The braiding on the even-even block.

theorem RS.SuperVect.koszul_oo {V W : SuperVect} (u : V.odd) (v : W.odd) : (V.koszulBraiding W).evenMap (0, u ⊗ₜ[ℂ] v) = (0, -v ⊗ₜ[ℂ] u)

The braiding on the odd-odd block: the Koszul sign.

theorem RS.SuperVect.koszul_eo {V W : SuperVect} (x : V.even) (v : W.odd) : (V.koszulBraiding W).oddMap (x ⊗ₜ[ℂ] v, 0) = (0, v ⊗ₜ[ℂ] x)

The braiding on the even-odd block.

theorem RS.SuperVect.koszul_oe {V W : SuperVect} (u : V.odd) (w : W.even) : (V.koszulBraiding W).oddMap (0, u ⊗ₜ[ℂ] w) = (w ⊗ₜ[ℂ] u, 0)

The braiding on the odd-even block.

theorem RS.SuperVect.assoc_unit_inv_ee {V : SuperVect} (r : ℂ) (x y : V.even) : (tensorUnit.associator V V).inv.evenMap (r ⊗ₜ[ℂ] (x ⊗ₜ[ℂ] y, 0), 0) = ((r ⊗ₜ[ℂ] x, 0) ⊗ₜ[ℂ] y, 0)

The unit-prefixed inverse associator on the even-even block.

theorem RS.SuperVect.assoc_unit_inv_oo {V : SuperVect} (r : ℂ) (u v : V.odd) : (tensorUnit.associator V V).inv.evenMap (r ⊗ₜ[ℂ] (0, u ⊗ₜ[ℂ] v), 0) = (0, (r ⊗ₜ[ℂ] u, 0) ⊗ₜ[ℂ] v)

The unit-prefixed inverse associator on the odd-odd block.

theorem RS.SuperVect.assoc_unit_inv_eo {V : SuperVect} (r : ℂ) (x : V.even) (v : V.odd) : (tensorUnit.associator V V).inv.oddMap (r ⊗ₜ[ℂ] (x ⊗ₜ[ℂ] v, 0), 0) = ((r ⊗ₜ[ℂ] x, 0) ⊗ₜ[ℂ] v, 0)

The unit-prefixed inverse associator on the even-odd block.

theorem RS.SuperVect.assoc_unit_inv_oe {V : SuperVect} (r : ℂ) (u : V.odd) (y : V.even) : (tensorUnit.associator V V).inv.oddMap (r ⊗ₜ[ℂ] (0, u ⊗ₜ[ℂ] y), 0) = (0, (r ⊗ₜ[ℂ] u, 0) ⊗ₜ[ℂ] y)

The unit-prefixed inverse associator on the odd-even block.