The symplectic Brauer crossing on a tensor power

The permutation diagrams of the Brauer algebra act on the d-th tensor power of the standard symplectic module V = k^{2n} not by the bare permutation of the tensor factors but by its sign twist: a permutation σ of the strands acts by sign σ times the reindexing of the slots along σ. That action, TauCeti.symplecticPermTensorAction, is the general sign-twisted permutation action PiTensorProduct.signReindexRepresentation at M = k^{2n}; this file proves the relations it satisfies with the symplectic arcs TauCeti.symplecticCupCapAt.

Why the sign

The cap and the cup of the standard alternating form each change sign when their two endpoints are exchanged. So the bare transposition of the two slots of an arc negates the arc instead of absorbing it, and it is minus that transposition which satisfies the Brauer relation s e = e. On two strands this is the crossing TauCeti.symplecticCrossing of TauCeti/RepresentationTheory/ClassicalGroups/BrauerGenerators/Symplectic/Basic.lean, which this file reproduces at d = 2 (TauCeti.symplecticPermTensorAction_swap_zero_one). On d strands the crossings must still satisfy the Coxeter relations of the symmetric group, so the transposition (i j) acting by minus the reindexing extends uniquely to σ ↦ sign σ • reindex σ: the sign twist is forced, not chosen.

The relations

Writing s σ for the action of the permutation σ and e i j for the arc on the strands i and j, the relations proved here are

• s σ * e i j = e (σ i) (σ j) * s σ, the renaming of the arc by a permutation of the strands;
• s (i j) * e i j = e i j and e i j * s (i j) = e i j, the two absorptions of the crossing on the arc;
• e i l * e i j = e i l * s (j l) for three distinct strands, both sides being the diagram with a cap on i, j, a cup on i, l and a through strand from l to j;
• the mixed relations s (i j) * e j l * e i j = s (j l) * e i j, e i j * e j l * s (i j) = e i j * s (j l) and e i j * s (j l) * e i j = e i j that follow;
• e i j * e j l * e i j = e i j, the absorption of two arcs sharing the strand j, which these give in a few rewrites.

Together with s being a monoid homomorphism, which gives s² = 1 and the braid relations, and with the relations among arcs alone of TauCeti/RepresentationTheory/ClassicalGroups/BrauerGenerators/Symplectic/TensorPower.lean, these are the relations of the Brauer algebra B_d(-2n) between crossings and arcs, at the symplectic loop value. That the crossings and arcs assemble into an algebra map from B_d(-2n) is not proved here. Finally s σ commutes with the diagonal action of every linear map, so in particular with the symplectic group.

Main definitions

• TauCeti.symplecticPermTensorAction: the sign-twisted permutation action of S_d on the d-th tensor power of k^{2n}.

Main results

• TauCeti.symplecticPermTensorAction_swap_zero_one: on two strands the transposition acts by the crossing TauCeti.symplecticCrossing.
• TauCeti.commute_symplecticPermTensorAction_tensorPower: the action commutes with the diagonal action of the symplectic group.
• TauCeti.symplecticPermTensorAction_mul_symplecticCupCapAt: the renaming relation.
• TauCeti.symplecticPermTensorAction_swap_mul_symplecticCupCapAt and TauCeti.symplecticCupCapAt_mul_symplecticPermTensorAction_swap: the crossing on an arc is absorbed.
• TauCeti.symplecticCupCapAt_mul_symplecticCupCapAt: two arcs sharing one strand compose to an arc followed by a crossing.
• TauCeti.symplecticPermTensorAction_swap_mul_symplecticCupCapAt_mul_symplecticCupCapAt, TauCeti.symplecticCupCapAt_mul_symplecticCupCapAt_mul_symplecticPermTensorAction_swap and TauCeti.symplecticCupCapAt_mul_symplecticPermTensorAction_swap_mul_symplecticCupCapAt: the mixed relations.
• TauCeti.symplecticCupCapAt_mul_mul_self: two arcs sharing a strand absorb, e i j * e j l * e i j = e i j.

References

• R. Brauer, On algebras which are connected with the semisimple continuous groups, Annals of Mathematics 38 (1937), 857-872.
• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants, Springer GTM 255 (2009), Chapter 10, for the Brauer algebra acting on the tensor powers of a symplectic space.

noncomputable def TauCeti.symplecticPermTensorAction (k : Type u) (n d : ℕ) [CommRing k] : Representation k (Equiv.Perm (Fin d)) (TensorPower k d (Fin n ⊕ Fin n → k))

The sign-twisted permutation action of the symmetric group S_d on the d-th tensor power of the standard symplectic module k^{2n}: the general PiTensorProduct.signReindexRepresentation at M = k^{2n}. This is the action of the permutation diagrams in the symplectic Brauer action; on two strands the transposition acts by TauCeti.symplecticCrossing.

theorem TauCeti.symplecticPermTensorAction_def (k : Type u) (n d : ℕ) [CommRing k] : symplecticPermTensorAction k n d = PiTensorProduct.signReindexRepresentation k (Fin n ⊕ Fin n → k) (Fin d)

The symplectic permutation action is the sign-twisted reindexing representation on the standard symplectic module.

@[simp]

theorem TauCeti.symplecticPermTensorAction_tprod {k : Type u} {n d : ℕ} [CommRing k] (σ : Equiv.Perm (Fin d)) (v : Fin d → Fin n ⊕ Fin n → k) : ((symplecticPermTensorAction k n d) σ) ((PiTensorProduct.tprod k) v) = ↑↑(Equiv.Perm.sign σ) • (PiTensorProduct.tprod k) fun (t : Fin d) => v ((Equiv.symm σ) t)

A permutation reindexes a pure tensor and multiplies it by its sign.

theorem TauCeti.symplecticPermTensorAction_swap_tprod {k : Type u} {n d : ℕ} [CommRing k] {i j : Fin d} (hij : i ≠ j) (v : Fin d → Fin n ⊕ Fin n → k) : ((symplecticPermTensorAction k n d) (Equiv.swap i j)) ((PiTensorProduct.tprod k) v) = -(PiTensorProduct.tprod k) fun (t : Fin d) => v ((Equiv.swap i j) t)

A transposition of distinct strands exchanges their factors in a pure tensor and negates it.

theorem TauCeti.symplecticPermTensorAction_swap_zero_one {k : Type u} {n : ℕ} [CommRing k] : (symplecticPermTensorAction k n 2) (Equiv.swap 0 1) = symplecticCrossing k n

On two strands the transposition acts by the Brauer crossing TauCeti.symplecticCrossing, minus the flip of the two tensor factors.

Commuting with the diagonal action

theorem TauCeti.commute_symplecticPermTensorAction_tensorPower {k : Type u} {n d : ℕ} [CommRing k] (σ : Equiv.Perm (Fin d)) (g : ↥(Matrix.symplecticGroup (Fin n) k)) : Commute ((symplecticPermTensorAction k n d) σ) (((stdSymplecticRep k n).tensorPower d) g)

The sign-twisted permutation action commutes with the symplectic group acting diagonally on the tensor power, so every permutation diagram acts by an intertwiner.

The crossing on an arc, and the renaming of an arc

theorem TauCeti.symplecticPermTensorAction_mul_symplecticCupCapAt {k : Type u} {n d : ℕ} [CommRing k] (σ : Equiv.Perm (Fin d)) (i j : Fin d) : (symplecticPermTensorAction k n d) σ * symplecticCupCapAt k n d i j = symplecticCupCapAt k n d (σ i) (σ j) * (symplecticPermTensorAction k n d) σ

The renaming relation: permuting the strands renames the arc, s σ * e i j = e (σ i) (σ j) * s σ. The sign of σ appears on both sides, so this is bookkeeping on the index set; it does not read the arc through the form and holds at coincident strands too.

@[simp]

theorem TauCeti.symplecticPermTensorAction_swap_mul_symplecticCupCapAt {k : Type u} {n d : ℕ} [CommRing k] (i j : Fin d) : (symplecticPermTensorAction k n d) (Equiv.swap i j) * symplecticCupCapAt k n d i j = symplecticCupCapAt k n d i j

The relation s e = e: the crossing of the two strands of an arc is absorbed by the cup on top of it. The bare transposition negates the cup, because the copairing is antisymmetric, and the sign of the transposition cancels that.

@[simp]

theorem TauCeti.symplecticCupCapAt_mul_symplecticPermTensorAction_swap {k : Type u} {n d : ℕ} [CommRing k] (i j : Fin d) : symplecticCupCapAt k n d i j * (symplecticPermTensorAction k n d) (Equiv.swap i j) = symplecticCupCapAt k n d i j

The relation e s = e: the crossing of the two strands of an arc is absorbed by the cap at the bottom of it. By the renaming relation the transposition of the two strands commutes with the arc, so this is TauCeti.symplecticPermTensorAction_swap_mul_symplecticCupCapAt read from the other side.

theorem TauCeti.commute_symplecticPermTensorAction_symplecticCupCapAt {k : Type u} {n d : ℕ} [CommRing k] {σ : Equiv.Perm (Fin d)} {i j : Fin d} (hσ : {σ i, σ j} = {i, j}) : Commute ((symplecticPermTensorAction k n d) σ) (symplecticCupCapAt k n d i j)

A permutation preserving the unordered pair of strands of an arc commutes with the arc. This includes the permutations fixing both strands and those exchanging them.

Two arcs sharing a strand

theorem TauCeti.symplecticCupCapAt_mul_symplecticCupCapAt {k : Type u} {n d : ℕ} [CommRing k] {i j l : Fin d} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) : symplecticCupCapAt k n d i l * symplecticCupCapAt k n d i j = symplecticCupCapAt k n d i l * (symplecticPermTensorAction k n d) (Equiv.swap j l)

Two arcs sharing one strand compose to an arc after a crossing: for three distinct strands, e i l * e i j = e i l * s (j l). Both sides are the diagram with a cap on i, j, a cup on i, l and a through strand from l to j. On the left the strand is the zigzag through the middle cup on i, j and the cap on i, l, which straightens by the column pairing Jᵀ * J = 1; on the right the crossing carries the slot l to the slot j, and its sign cancels the sign of the two cups.

The mixed relations

theorem TauCeti.symplecticPermTensorAction_swap_mul_symplecticCupCapAt_mul_symplecticCupCapAt {k : Type u} {n d : ℕ} [CommRing k] {i j l : Fin d} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) : (symplecticPermTensorAction k n d) (Equiv.swap i j) * (symplecticCupCapAt k n d j l * symplecticCupCapAt k n d i j) = (symplecticPermTensorAction k n d) (Equiv.swap j l) * symplecticCupCapAt k n d i j

The mixed Brauer relation sᵢ eᵢ₊₁ eᵢ = sᵢ₊₁ eᵢ, on any three distinct strands. Moving the crossings past the arcs by the renaming relation, both sides become TauCeti.symplecticCupCapAt_mul_symplecticCupCapAt.

theorem TauCeti.symplecticCupCapAt_mul_symplecticCupCapAt_mul_symplecticPermTensorAction_swap {k : Type u} {n d : ℕ} [CommRing k] {i j l : Fin d} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) : symplecticCupCapAt k n d i j * symplecticCupCapAt k n d j l * (symplecticPermTensorAction k n d) (Equiv.swap i j) = symplecticCupCapAt k n d i j * (symplecticPermTensorAction k n d) (Equiv.swap j l)

The mixed Brauer relation eᵢ eᵢ₊₁ sᵢ = eᵢ sᵢ₊₁, the reverse product form of TauCeti.symplecticPermTensorAction_swap_mul_symplecticCupCapAt_mul_symplecticCupCapAt, on any three distinct strands.

@[simp]

theorem TauCeti.symplecticCupCapAt_mul_symplecticPermTensorAction_swap_mul_symplecticCupCapAt {k : Type u} {n d : ℕ} [CommRing k] {i j l : Fin d} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) : symplecticCupCapAt k n d i j * (symplecticPermTensorAction k n d) (Equiv.swap j l) * symplecticCupCapAt k n d i j = symplecticCupCapAt k n d i j

The mixed Brauer relation eᵢ sᵢ₊₁ eᵢ = eᵢ, on any three distinct strands: a crossing between two copies of an arc, on a strand of the arc and a third strand, straightens out.

Two arcs sharing a strand absorb

theorem TauCeti.symplecticCupCapAt_mul_mul_self {k : Type u} {n d : ℕ} [CommRing k] {i j l : Fin d} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) : symplecticCupCapAt k n d i j * symplecticCupCapAt k n d j l * symplecticCupCapAt k n d i j = symplecticCupCapAt k n d i j

Two arcs sharing one strand: e i j * e j l * e i j = e i j, the relation that makes two generators on overlapping pairs of strands absorb one another. Composing the two arcs on the right gives an arc after the crossing s (i l) by TauCeti.symplecticCupCapAt_mul_symplecticCupCapAt; the renaming relation moves that crossing past the arc e j l, and the mixed relation e j i * s (i l) * e j i = e j i closes it.