Chevalley commutator relations in the symplectic group

This file proves the rank-two, multiply-laced commutator relations among the explicit root subgroups of TauCeti.GLSymplecticFin. For distinct i and j, the roots eᵢ - eⱼ, 2eⱼ, eᵢ + eⱼ, and 2eᵢ form a type-C₂ root string, and the chosen matrix parametrizations satisfy

⁅x_{eᵢ-eⱼ}(a), x_{2eⱼ}(b)⁆
  = x_{eᵢ+eⱼ}(ab) x_{2eᵢ}(a²b).

The opposite-root-string analogues are

⁅x_{eᵢ-eⱼ}(a), x_{-2eᵢ}(b)⁆
  = x_{-eᵢ-eⱼ}(-ab) x_{-2eⱼ}(a²b),
⁅x_{eᵢ-eⱼ}(a), x_{-eᵢ-eⱼ}(b)⁆ = x_{-2eⱼ}(-2ab).

The second relation in each root string records its non-unit structure constant; for the positive string it is

⁅x_{eᵢ-eⱼ}(a), x_{eᵢ+eⱼ}(b)⁆ = x_{2eᵢ}(2ab).

Together these four identities are the rank-two relations needed to compare the standard symplectic realization with the characteristic-two special isogeny of type B₂/C₂.

The complementary long-root strings, starting from the sum roots, are

⁅x_{eᵢ+eⱼ}(a), x_{-2eⱼ}(b)⁆
  = x_{eᵢ-eⱼ}(ab) x_{2eᵢ}(-a²b),
⁅x_{-eᵢ-eⱼ}(a), x_{2eⱼ}(b)⁆
  = x_{eⱼ-eᵢ}(-ab) x_{-2eᵢ}(-a²b).

Thus every interaction between a long root and a nonopposite short root in the rank-two subsystem is available without changing coordinates.

The type-A subsystem of difference roots also satisfies the structure-constant-one relation

⁅x_{eᵢ-eⱼ}(a), x_{eⱼ-eₖ}(b)⁆ = x_{eᵢ-eₖ}(ab).

References

• R. W. Carter, Simple Groups of Lie Type (1972), §5.2 and §11.3.
• J. E. Humphreys, Linear Algebraic Groups (1975), §26.3.
• R. Steinberg, Lectures on Chevalley Groups (1968), §§3--4.

theorem TauCeti.GLSymplecticFin.commutatorElement_differenceShortRootUnit_differenceShortRootUnit {R : Type u} [CommRing R] {m : ℕ} {i j k : Fin m} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (a b : R) : ⁅differenceShortRootUnit hij a, differenceShortRootUnit hjk b⁆ = differenceShortRootUnit hik (a * b)

The structure-constant-one Chevalley relation in the difference-root subsystem. For pairwise distinct indices, the commutator of x_{eᵢ-eⱼ}(a) and x_{eⱼ-eₖ}(b) is x_{eᵢ-eₖ}(ab).

theorem TauCeti.GLSymplecticFin.commutatorElement_differenceShortRootUnit_positiveLongRootTransvectionUnit {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (a b : R) : ⁅differenceShortRootUnit hij a, positiveLongRootTransvectionUnit j b⁆ = positiveSumShortRootUnit hij (a * b) * positiveLongRootTransvectionUnit i (a ^ 2 * b)

The multiply-laced Chevalley relation in the standard symplectic group. The commutator of x_{eᵢ-eⱼ}(a) and x_{2eⱼ}(b) is the product of the two remaining root subgroups in their root string, with parameters ab and a²b.

theorem TauCeti.GLSymplecticFin.commutatorElement_differenceShortRootUnit_positiveSumShortRootUnit {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (a b : R) : ⁅differenceShortRootUnit hij a, positiveSumShortRootUnit hij b⁆ = positiveLongRootTransvectionUnit i (2 * a * b)

The structure-constant-two Chevalley relation in the standard symplectic group. The commutator of x_{eᵢ-eⱼ}(a) and x_{eᵢ+eⱼ}(b) is x_{2eᵢ}(2ab).

theorem TauCeti.GLSymplecticFin.commutatorElement_differenceShortRootUnit_negativeLongRootTransvectionUnit {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (a b : R) : ⁅differenceShortRootUnit hij a, negativeLongRootTransvectionUnit i b⁆ = negativeSumShortRootUnit hij (-(a * b)) * negativeLongRootTransvectionUnit j (a ^ 2 * b)

The negative multiply-laced Chevalley relation in the standard symplectic group. The commutator of x_{eᵢ-eⱼ}(a) and x_{-2eᵢ}(b) is the product of the two remaining root subgroups in their root string, with parameters -ab and a²b.

theorem TauCeti.GLSymplecticFin.commutatorElement_differenceShortRootUnit_negativeSumShortRootUnit {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (a b : R) : ⁅differenceShortRootUnit hij a, negativeSumShortRootUnit hij b⁆ = negativeLongRootTransvectionUnit j (-(2 * a * b))

The negative structure-constant-two Chevalley relation in the standard symplectic group. The commutator of x_{eᵢ-eⱼ}(a) and x_{-eᵢ-eⱼ}(b) is x_{-2eⱼ}(-2ab).

theorem TauCeti.GLSymplecticFin.commutatorElement_positiveSumShortRootUnit_negativeLongRootTransvectionUnit {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (a b : R) : ⁅positiveSumShortRootUnit hij a, negativeLongRootTransvectionUnit j b⁆ = differenceShortRootUnit hij (a * b) * positiveLongRootTransvectionUnit i (-(a ^ 2 * b))

The complementary positive-sum multiply-laced Chevalley relation. The commutator of x_{eᵢ+eⱼ}(a) and x_{-2eⱼ}(b) is the product of the root subgroups for eᵢ-eⱼ and 2eᵢ, with parameters ab and -a²b.

theorem TauCeti.GLSymplecticFin.commutatorElement_negativeSumShortRootUnit_positiveLongRootTransvectionUnit {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (a b : R) : ⁅negativeSumShortRootUnit hij a, positiveLongRootTransvectionUnit j b⁆ = differenceShortRootUnit ⋯ (-(a * b)) * negativeLongRootTransvectionUnit i (-(a ^ 2 * b))

The complementary negative-sum multiply-laced Chevalley relation. The commutator of x_{-eᵢ-eⱼ}(a) and x_{2eⱼ}(b) is the product of the root subgroups for eⱼ-eᵢ and -2eᵢ, both with the signs forced by the chosen parametrizations.