Generating the difference-root subgroups of the symplectic group

For the standard type-C_m root system, the roots eᵢ - eⱼ form its type-A_(m-1) subsystem, whose structure-constant-one Chevalley relation is

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

This file uses it to show that a subgroup containing the difference-root elements at adjacent indices, in both orientations, contains every difference-root element. This is the first generation step for identifying the full-weight type-C Chevalley carrier with the standard symplectic group: the numbered short simple roots are adjacent difference roots, while the remaining simple root is long.

Main results

• TauCeti.GLSymplecticFin.differenceShortRootUnit_mem_of_adjacent: adjacent difference-root subgroups generate all difference-root subgroups.

References

• R. W. Carter, Simple Groups of Lie Type (1972), §5.2.
• R. Steinberg, Lectures on Chevalley Groups (1968), §§3--4.

This advances Layer 9, "The Chevalley--Demazure construction", of TauCetiRoadmap/ReductiveGroups/README.md: it supplies the type-A subsystem generation needed to identify the explicit full-weight type-C carrier on field-valued points.

theorem TauCeti.GLSymplecticFin.differenceShortRootUnit_mem_of_adjacent {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (hadjacent : ∀ {i j : Fin m} (hij : i ≠ j) (c : R), ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → differenceShortRootUnit hij c ∈ H) {i j : Fin m} (hij : i ≠ j) (c : R) : differenceShortRootUnit hij c ∈ H

If a subgroup of the standard symplectic group contains every adjacent difference-root element in both orientations, then it contains every difference-root element.