The sign-twisted permutation action on a tensor power

A permutation σ of a finite index type ι acts on the tensor power ⨂[R] _ : ι, M of any module by reindexing the tensor factors, PiTensorProduct.reindexRepresentation. This file twists that action by the sign character: σ acts by sign σ times the reindexing. It is Representation.charTwist of the reindexing representation by TauCeti.signLinearCharacter, so it is again a representation, and it still commutes with the diagonal action of every linear map since the sign is a scalar.

This is the action of the permutation diagrams of the Brauer algebra on the tensor powers of a symplectic module, where the crossing must carry a sign to be absorbed by the alternating arcs; see TauCeti/RepresentationTheory/ClassicalGroups/BrauerGenerators/Symplectic/Crossing.lean.

Main definitions

• PiTensorProduct.signReindexRepresentation: the sign-twisted permutation action of Equiv.Perm ι on ⨂[R] _ : ι, M.

Main results

• PiTensorProduct.signReindexRepresentation_tprod: a permutation reindexes a pure tensor and multiplies it by its sign.
• PiTensorProduct.signReindexRepresentation_swap and PiTensorProduct.signReindexRepresentation_swap_tprod: a transposition of two distinct factors acts by minus the reindexing.
• PiTensorProduct.commute_signReindexRepresentation_map: the action commutes with applying the same linear map in every tensor factor.

noncomputable def PiTensorProduct.signReindexRepresentation (R : Type u) (M : Type v) (ι : Type w) [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] [Fintype ι] : Representation R (Equiv.Perm ι) (PiTensorProduct R fun (x : ι) => M)

The sign-twisted permutation action of Equiv.Perm ι on the ι-indexed tensor power of M: a permutation reindexes the tensor factors and multiplies by its sign.

theorem PiTensorProduct.signReindexRepresentation_apply {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) : (signReindexRepresentation R M ι) σ = ↑↑(Equiv.Perm.sign σ) • ↑(reindex R (fun (x : ι) => M) σ)

A permutation acts by its sign times PiTensorProduct.reindex.

@[simp]

theorem PiTensorProduct.signReindexRepresentation_tprod {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) (v : ι → M) : ((signReindexRepresentation R M ι) σ) ((tprod R) v) = ↑↑(Equiv.Perm.sign σ) • (tprod R) fun (t : ι) => v ((Equiv.symm σ) t)

A permutation on a pure tensor: the factors are reindexed and the result is multiplied by the sign of the permutation.

theorem PiTensorProduct.signReindexRepresentation_swap {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] [Fintype ι] {i j : ι} (hij : i ≠ j) : (signReindexRepresentation R M ι) (Equiv.swap i j) = -↑(reindex R (fun (x : ι) => M) (Equiv.swap i j))

A transposition of two distinct factors acts by minus the reindexing.

theorem PiTensorProduct.signReindexRepresentation_swap_tprod {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] [Fintype ι] {i j : ι} (hij : i ≠ j) (v : ι → M) : ((signReindexRepresentation R M ι) (Equiv.swap i j)) ((tprod R) v) = -(tprod R) fun (t : ι) => v ((Equiv.swap i j) t)

A transposition of two distinct factors on a pure tensor exchanges the two factors and changes the sign.

theorem PiTensorProduct.commute_signReindexRepresentation_map {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) (f : M →ₗ[R] M) : Commute ((signReindexRepresentation R M ι) σ) (map fun (x : ι) => f)

The sign-twisted permutation action commutes with the diagonal action of every linear map: permuting the tensor factors commutes with applying the same map in each of them, and the sign is a scalar.