Brauer duality for the symplectic group on two strands

Let V = K^{2n} carry the standard alternating form of Matrix.J. The Brauer algebra B₂(-2n) acts on V ⊗ V through its three diagrams: the identity, the crossing TauCeti.symplecticCrossing, which is minus the flip of the two factors (the sign forced by the alternating form), and the cap-cup diagram TauCeti.symplecticCupCap, which contracts the two factors against the form and re-expands them through the invariant bivector. All three commute with the diagonal action of the symplectic group. This file proves the converse on two strands: every operator on V ⊗ V commuting with the symplectic group is a combination of the three (TauCeti.mem_centralizer_stdSymplecticRep_tensorPower_two_iff), so the commutant is the algebra generated by the crossing and the cap-cup diagram (TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer). This is the two-strand case of the theorem that the image of B_k(-2n) is the commutant of the symplectic group on V^{⊗k}, and the symplectic counterpart of Brauer duality for the orthogonal group on two strands.

The theorem holds over every integral domain containing a unit t with t ^ m ≠ 1 for 0 < m ≤ 4, for instance over any field of characteristic zero, with t = 2 (TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer_of_charZero). The unit is used only to build a diagonal symplectic matrix whose eigenvalues separate the weights of V ⊗ V.

The argument

In the monomial basis of the tensors e_p ⊗ e_q, an operator on V ⊗ V is a matrix M whose rows and columns are indexed by words of two labels in Fin n ⊕ Fin n, and commuting with g ⊗ g is commuting with the Kronecker square of g (Matrix.toMatrix_piTensorProductMap_mulVecLin).

• Monomial symplectic matrices. A monomial matrix e_y ↦ d y • e_(π y) is symplectic when it preserves the entries of J up to the weights d. Commuting with its Kronecker square relabels the entries of M by π, up to nonzero factors (Matrix.apply_comp_mul_prod_of_commute_kroneckerPower), so it preserves their vanishing. The permutations of the n pairs (inl i, inr i), the exchanges of the two labels of one pair (with a sign) and the diagonal matrices scaling a label by t and its partner by t⁻¹ are of this kind.
• Weights. The diagonal matrices force an entry of M to vanish unless its row and column have the same weight. As t has no small power equal to 1, this leaves the entries where the column word is the row word, or its reversal, or where both words are pairs (x, x.swap).
• Normal forms. The permutations of the pairs and the exchanges within a pair move any such entry to one of six normal forms, at the labels a = inl i₀, b = inr i₀ and, when a second pair is needed, c = inl j, d = inr j.
• Unipotent relations. Two upper unitriangular symplectic matrices fromBlocks 1 B 0 1 express the normal forms at (a, a), at (a, c) and at its reversal through the three normal forms at (a, b) and (b, a) against (a, b) and at (c, d) against (a, b).

Subtracting the combination of the identity, the crossing and the cap-cup diagram that matches M at those three entries leaves a matrix that commutes with the symplectic group and vanishes there, hence everywhere.

Main results

• TauCeti.mem_centralizer_stdSymplecticRep_tensorPower_two_iff: the operators commuting with the symplectic group on two strands are the combinations of the identity, the crossing and the cap-cup diagram.
• TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer: Brauer duality for the symplectic group on two strands, the commutant is generated by the two Brauer diagrams.
• TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer_of_charZero: the same over a field of characteristic zero, such as ℂ.

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), Chapters 5 and 10.

Monomial symplectic matrices

Weights

Matrices commuting with the symplectic group on two strands

Brauer duality on two strands

theorem TauCeti.mem_centralizer_stdSymplecticRep_tensorPower_two_iff {K : Type u_1} [CommRing K] {n : ℕ} [IsDomain K] (ht : ∃ (t : Kˣ), ∀ (m : ℕ), 0 < m → m ≤ 4 → t ^ m ≠ 1) (T : Module.End K (TensorPower K 2 (Fin n ⊕ Fin n → K))) : T ∈ Subalgebra.centralizer K (Set.range ⇑((stdSymplecticRep K n).tensorPower 2)) ↔ ∃ (x : K) (y : K) (z : K), T = x • 1 + y • symplecticCrossing K n + z • symplecticCupCap K n

The commutant of the symplectic group on two strands. Over an integral domain containing a unit t with t ^ m ≠ 1 for 0 < m ≤ 4, an operator on K^{2n} ⊗ K^{2n} commutes with the diagonal action of the symplectic group exactly when it is a combination of the identity, the Brauer crossing TauCeti.symplecticCrossing (minus the flip of the two factors) and the cap-cup diagram TauCeti.symplecticCupCap (the contraction against the alternating form followed by the insertion of the invariant bivector).

theorem TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer {K : Type u_1} [CommRing K] {n : ℕ} [IsDomain K] (ht : ∃ (t : Kˣ), ∀ (m : ℕ), 0 < m → m ≤ 4 → t ^ m ≠ 1) : K[symplecticCrossing K n, symplecticCupCap K n] = Subalgebra.centralizer K (Set.range ⇑((stdSymplecticRep K n).tensorPower 2))

Brauer duality for the symplectic group on two strands. Over an integral domain containing a unit t with t ^ m ≠ 1 for 0 < m ≤ 4, the operators on K^{2n} ⊗ K^{2n} commuting with the diagonal action of the symplectic group form the algebra generated by the two Brauer diagrams on two strands other than the identity: the crossing TauCeti.symplecticCrossing and the cap-cup diagram TauCeti.symplecticCupCap.

theorem TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer_of_charZero {K : Type u_1} [Field K] [CharZero K] {n : ℕ} : K[symplecticCrossing K n, symplecticCupCap K n] = Subalgebra.centralizer K (Set.range ⇑((stdSymplecticRep K n).tensorPower 2))

Brauer duality for the symplectic group on two strands in characteristic zero, for instance over ℂ: the unit 2 has no nontrivial power equal to 1.