The cap, the cup, and the Brauer relations on the symplectic tensor square

The symplectic group acts on V = k^{2n} preserving the standard alternating form of Matrix.J, and that form is a map V ⊗ V → k: read as a diagram it is a cap, an arc joining the two bottom points. The matrix -J, read as a bivector 1 ↦ ∑ₓ ∑_y (-J) x y • eₓ ⊗ e_y, is the same arc drawn at the top, the cup k → V ⊗ V. Composing a cap with a cup gives the Brauer diagram e on two strands, and permuting the two tensor factors gives, up to a sign, the crossing s. Together with the identity these are the three Brauer diagrams on two strands, and this file proves the three relations they satisfy on V^{⊗2},

s * s = 1, e * e = δ • e, s * e = e * s = e, with the loop value δ = -2n = -dim V,

together with the invariance of the cap and the cup under the symplectic group, from which both generators commute with the diagonal symplectic action.

The sign convention

The orthogonal story of TauCeti.RepresentationTheory.ClassicalGroups.BrauerGenerators.Orthogonal.Basic is repeated here with one genuine change, and it is a change of sign. The coordinate dot product is symmetric, so there the crossing is the bare flip of the two tensor factors. The standard symplectic form is alternating, so the bare flip TauCeti.symplecticFlip anticommutes with the cap and with the cup (TauCeti.symplecticCap_comp_symplecticFlip and TauCeti.symplecticFlip_comp_symplecticCup), and the relations s * e = e = e * s fail for it. The Brauer crossing is therefore taken to be minus the flip, TauCeti.symplecticCrossing, and with that choice all three relations hold. This is the sign that has to be fixed before a Brauer action on V^{⊗k} is well defined.

The sign is forced, not chosen. The two anti-invariances give flip * e = -e, so if the bare flip were the crossing then s * e = e would force 2 • e = 0, which is false over ℂ for n ≥ 1 because cap ∘ e ∘ cup is multiplication by (-2n)^2. Re-ordering the arcs does not repair it: each of the two orderings only changes cap or cup by a sign, which changes e by a sign at most and leaves cap ∘ flip = -cap and flip ∘ cup = -cup -- hence flip * e = -e -- intact. So on the permutation diagrams the symplectic Brauer action is the sign-twisted permutation action rather than the bare one; that twist is the standard symplectic convention, and it is the same phenomenon that makes the Brauer parameter negative.

The loop value is negative for the same reason. A closed loop is a cup stacked under a cap, so it contracts the pairing J against the copairing -J, and that contraction is -∑ₓ ∑_y (J x y) * (J x y) = -tr (J * Jᵀ) = -tr 1 = -2n. It is -dim V rather than dim V; it is not the trace of J, which vanishes.

Implementation notes

The alternating form needs subtraction, so, unlike the orthogonal file, the cap, the cup, the crossing and the Brauer relations are stated over a commutative ring rather than a commutative semiring. The flip of the two tensor factors and its involutivity carry no sign, so they are stated over a commutative semiring.

The two invariance statements are recorded for a bare matrix rather than only for an element of Matrix.symplecticGroup (Fin n) k, because they consume the defining identity from opposite sides: the cap is preserved by every A with Aᵀ * J * A = J, and the cup by every A with A * J * Aᵀ = J. The two conditions are equivalent, and Mathlib records both (SymplecticGroup.mem_iff' and SymplecticGroup.mem_iff), but which side a proof uses is the visible difference between contracting a pair of inputs and expanding a pair of outputs.

The flip is given a name of its own, unlike in the orthogonal file, for two reasons: it differs from the Brauer crossing by the sign above, and the Layer 8 action TauCeti.permTensorAction is set up for the coordinate space Fin n → k, so it does not apply to the symplectic (Fin n ⊕ Fin n) → k.

The index set is Fin n ⊕ Fin n rather than a general l ⊕ l, even though Matrix.J and Matrix.symplecticGroup are defined for a general l, because the invariant form TauCeti.stdSymplecticBilinForm and the standard representation TauCeti.stdSymplecticRep that this file consumes are pinned at Fin n.

The bookkeeping for pure tensors on two strands carries no symplectic content and lives in TauCeti.LinearAlgebra.PiTensorProduct.TwoStrand. This file consumes one lemma from there, Matrix.piTensorProductMap_bivector, which pushes a whole bivector through the tensor square; the orthogonal file consumes the pointwise Matrix.piTensorProductMap_tprod_single together with TauCeti.tprod_fin_two, and TauCeti.sum_pi_fin_two supports Matrix.piTensorProductMap_tprod_single from inside that module.

Main definitions

• TauCeti.symplecticCap: the cap V ⊗ V → k, the standard alternating form.
• TauCeti.symplecticCup: the cup k → V ⊗ V, the bivector of -J.
• TauCeti.symplecticCupCap: the Brauer generator e, the composite cup ∘ₗ cap.
• TauCeti.symplecticFlip: the flip of the two tensor factors.
• TauCeti.symplecticCrossing: the Brauer generator s, minus the flip.

Main results

• TauCeti.symplecticCap_comp_symplecticCup: the loop value, cap ∘ cup = -2n.
• TauCeti.symplecticCupCap_mul_self: e * e = (-2n) • e.
• TauCeti.symplecticCrossing_mul_self: s * s = 1.
• TauCeti.symplecticCrossing_mul_symplecticCupCap and TauCeti.symplecticCupCap_mul_symplecticCrossing: s * e = e and e * s = e.
• TauCeti.symplecticCap_comp_piTensorProductMap and TauCeti.piTensorProductMap_comp_symplecticCup: the cap and the cup are invariant.
• TauCeti.commute_symplecticCupCap_tensorPower and TauCeti.commute_symplecticCrossing_tensorPower: both generators commute with the diagonal action of the symplectic group.

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 9.
• Schur--Weyl roadmap, Layer 9, "The invariant form and the action on V^{⊗k}", the symplectic case.

noncomputable def TauCeti.symplecticFlip (k : Type u) (n : ℕ) [CommSemiring k] : Module.End k (TensorPower k 2 (Fin n ⊕ Fin n → k))

The flip of the two tensor factors of V^{⊗2}. It is not the Brauer crossing: the crossing is its negative, see TauCeti.symplecticCrossing.

Equations

• TauCeti.symplecticFlip k n = (PiTensorProduct.reindexRepresentation k (Fin n ⊕ Fin n → k) (Fin 2)) (Equiv.swap 0 1)

@[simp]

theorem TauCeti.symplecticFlip_tprod (k : Type u) (n : ℕ) [CommSemiring k] (v : Fin 2 → Fin n ⊕ Fin n → k) : (symplecticFlip k n) ((PiTensorProduct.tprod k) v) = (PiTensorProduct.tprod k) ![v 1, v 0]

@[simp]

theorem TauCeti.symplecticFlip_mul_self (k : Type u) (n : ℕ) [CommSemiring k] : symplecticFlip k n * symplecticFlip k n = 1

The flip is an involution: swapping the two tensor factors twice is the identity.

noncomputable def TauCeti.symplecticCap (k : Type u) (n : ℕ) [CommRing k] : TensorPower k 2 (Fin n ⊕ Fin n → k) →ₗ[k] k

The cap: the standard alternating form, read as a linear map on the tensor square. It is the invariant form of the symplectic group, drawn as an arc joining the two bottom points of a Brauer diagram.

Equations

• TauCeti.symplecticCap k n = PiTensorProduct.lift (TauCeti.symplecticCapMultilinear✝ k n)

@[simp]

theorem TauCeti.symplecticCap_tprod (k : Type u) (n : ℕ) [CommRing k] (v : Fin 2 → Fin n ⊕ Fin n → k) : (symplecticCap k n) ((PiTensorProduct.tprod k) v) = ((stdSymplecticBilinForm k n) (v 0)) (v 1)

theorem TauCeti.symplecticCap_tprod_single (k : Type u) (n : ℕ) [CommRing k] (x y : Fin n ⊕ Fin n) : (symplecticCap k n) ((PiTensorProduct.tprod k) ![Pi.single x 1, Pi.single y 1]) = Matrix.J (Fin n) k x y

The cap on a pair of standard basis vectors reads off the matrix entry of J.

noncomputable def TauCeti.symplecticCup (k : Type u) (n : ℕ) [CommRing k] : k →ₗ[k] TensorPower k 2 (Fin n ⊕ Fin n → k)

The cup: minus the bivector of J, that is the bivector of -J, drawn as an arc joining the two top points of a Brauer diagram. Since Matrix.J_squared gives J * J = -1, the matrix -J is the inverse J⁻¹, so this is the copairing inverse to the pairing that the cap contracts against. It is not a two-sided inverse of TauCeti.symplecticCap as a linear map -- as a pairing and a copairing the two have different sources and targets, and TauCeti.symplecticCap_comp_symplecticCup computes their composite to be multiplication by -2n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.symplecticCup_apply (k : Type u) (n : ℕ) [CommRing k] (c : k) : (symplecticCup k n) c = c • -∑ x : Fin n ⊕ Fin n, ∑ y : Fin n ⊕ Fin n, Matrix.J (Fin n) k x y • (PiTensorProduct.tprod k) ![Pi.single x 1, Pi.single y 1]

theorem TauCeti.symplecticCup_apply_one (k : Type u) (n : ℕ) [CommRing k] : (symplecticCup k n) 1 = -∑ x : Fin n ⊕ Fin n, ∑ y : Fin n ⊕ Fin n, Matrix.J (Fin n) k x y • (PiTensorProduct.tprod k) ![Pi.single x 1, Pi.single y 1]

theorem TauCeti.symplecticCap_comp_symplecticCup_apply (k : Type u) (n : ℕ) [CommRing k] (c : k) : (symplecticCap k n) ((symplecticCup k n) c) = -(2 * ↑n) * c

The loop value. A cup stacked under a cap closes into a loop, and the loop contracts the pairing J against the copairing -J: the value is -∑ₓ ∑_y (J x y) * (J x y), which is -tr (J * Jᵀ) = -tr 1 = -2n.

theorem TauCeti.symplecticCap_comp_symplecticCup (k : Type u) (n : ℕ) [CommRing k] : symplecticCap k n ∘ₗ symplecticCup k n = -(2 * ↑n) • LinearMap.id

The loop value, as an identity of linear maps: cap ∘ cup is multiplication by -2n.

noncomputable def TauCeti.symplecticCupCap (k : Type u) (n : ℕ) [CommRing k] : Module.End k (TensorPower k 2 (Fin n ⊕ Fin n → k))

The Brauer generator e on two strands: a cap on the two inputs followed by a cup on the two outputs. The name follows the written order of the composite cup ∘ₗ cap, as in TauCeti.symplecticCap_comp_symplecticCup for the loop.

Equations

• TauCeti.symplecticCupCap k n = TauCeti.symplecticCup k n ∘ₗ TauCeti.symplecticCap k n

@[simp]

theorem TauCeti.symplecticCupCap_apply (k : Type u) (n : ℕ) [CommRing k] (x : TensorPower k 2 (Fin n ⊕ Fin n → k)) : (symplecticCupCap k n) x = (symplecticCup k n) ((symplecticCap k n) x)

@[simp]

theorem TauCeti.symplecticCupCap_mul_self (k : Type u) (n : ℕ) [CommRing k] : symplecticCupCap k n * symplecticCupCap k n = -(2 * ↑n) • symplecticCupCap k n

The relation e² = δ e at the loop value δ = -2n: the middle of e * e is a closed loop.

noncomputable def TauCeti.symplecticCrossing (k : Type u) (n : ℕ) [CommRing k] : Module.End k (TensorPower k 2 (Fin n ⊕ Fin n → k))

The Brauer crossing s on two strands: minus the flip of the two tensor factors. The sign is forced by the alternating form; see the module docstring.

Equations

• TauCeti.symplecticCrossing k n = -TauCeti.symplecticFlip k n

@[simp]

theorem TauCeti.symplecticCrossing_tprod (k : Type u) (n : ℕ) [CommRing k] (v : Fin 2 → Fin n ⊕ Fin n → k) : (symplecticCrossing k n) ((PiTensorProduct.tprod k) v) = -(PiTensorProduct.tprod k) ![v 1, v 0]

The crossing swaps the two factors of a pure tensor and changes its sign.

@[simp]

theorem TauCeti.symplecticCrossing_mul_self (k : Type u) (n : ℕ) [CommRing k] : symplecticCrossing k n * symplecticCrossing k n = 1

The relation s² = 1: the crossing is an involution. The two signs cancel, so this is the bare statement that the flip is an involution.

theorem TauCeti.symplecticFlip_comp_symplecticCup (k : Type u) (n : ℕ) [CommRing k] : symplecticFlip k n ∘ₗ symplecticCup k n = -symplecticCup k n

The flip antifixes the cup: swapping the two top points of the arc reverses its orientation, because the bivector of J is antisymmetric.

theorem TauCeti.symplecticCap_comp_symplecticFlip (k : Type u) (n : ℕ) [CommRing k] : symplecticCap k n ∘ₗ symplecticFlip k n = -symplecticCap k n

The flip antifixes the cap: the standard symplectic form is alternating.

theorem TauCeti.symplecticCrossing_comp_symplecticCup (k : Type u) (n : ℕ) [CommRing k] : symplecticCrossing k n ∘ₗ symplecticCup k n = symplecticCup k n

The crossing fixes the cup: the two sign changes cancel.

theorem TauCeti.symplecticCap_comp_symplecticCrossing (k : Type u) (n : ℕ) [CommRing k] : symplecticCap k n ∘ₗ symplecticCrossing k n = symplecticCap k n

The crossing fixes the cap: the two sign changes cancel.

@[simp]

theorem TauCeti.symplecticCrossing_mul_symplecticCupCap (k : Type u) (n : ℕ) [CommRing k] : symplecticCrossing k n * symplecticCupCap k n = symplecticCupCap k n

The relation s e = e: the crossing is absorbed by the cup on top of e.

@[simp]

theorem TauCeti.symplecticCupCap_mul_symplecticCrossing (k : Type u) (n : ℕ) [CommRing k] : symplecticCupCap k n * symplecticCrossing k n = symplecticCupCap k n

The relation e s = e: the crossing is absorbed by the cap at the bottom of e.

theorem TauCeti.symplecticCap_comp_piTensorProductMap {k : Type u} {n : ℕ} [CommRing k] {A : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) k} (hA : A.transpose * Matrix.J (Fin n) k * A = Matrix.J (Fin n) k) : (symplecticCap k n ∘ₗ PiTensorProduct.map fun (x : Fin 2) => A.mulVecLin) = symplecticCap k n

The cap is invariant under every matrix A with Aᵀ * J * A = J: such a matrix preserves the standard alternating form, which is what the cap contracts against.

theorem TauCeti.piTensorProductMap_comp_symplecticCup {k : Type u} {n : ℕ} [CommRing k] {A : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) k} (hA : A * Matrix.J (Fin n) k * A.transpose = Matrix.J (Fin n) k) : (PiTensorProduct.map fun (x : Fin 2) => A.mulVecLin) ∘ₗ symplecticCup k n = symplecticCup k n

The cup is invariant under every matrix A with A * J * Aᵀ = J. This is the other one-sided identity: the cap consumes Aᵀ * J * A = J and the cup consumes A * J * Aᵀ = J.

theorem TauCeti.symplecticCap_comp_tensorPower (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : symplecticCap k n ∘ₗ ((stdSymplecticRep k n).tensorPower 2) g = symplecticCap k n

The cap is invariant under the diagonal action of the symplectic group.

theorem TauCeti.tensorPower_comp_symplecticCup (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : ((stdSymplecticRep k n).tensorPower 2) g ∘ₗ symplecticCup k n = symplecticCup k n

The cup is invariant under the diagonal action of the symplectic group.

theorem TauCeti.commute_symplecticCupCap_tensorPower (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : Commute (symplecticCupCap k n) (((stdSymplecticRep k n).tensorPower 2) g)

The Brauer generator e commutes with the symplectic group. This is the two-strand case of the statement that the diagram action and the symplectic action centralize one another.

theorem TauCeti.commute_symplecticFlip_tensorPower (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : Commute (symplecticFlip k n) (((stdSymplecticRep k n).tensorPower 2) g)

The flip commutes with the diagonal action of the symplectic group: permuting the tensor factors commutes with applying the same matrix in each of them.

theorem TauCeti.commute_symplecticCrossing_tensorPower (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : Commute (symplecticCrossing k n) (((stdSymplecticRep k n).tensorPower 2) g)

The Brauer generator s commutes with the symplectic group, the sign being central.