Generating the symplectic diagonal torus by root subgroups

Over a field, the standard symplectic group is generated by its positive and negative simple-root subgroups. The Gaussian decomposition reduces this statement to showing that the diagonal general-linear Levi elements already lie in the root-generated subgroup.

For a coordinate i and a unit a, the rank-one identity

diag(a, a⁻¹) = x₊(a) x₋(-a⁻¹) x₊(a) x₊(-1) x₋(1) x₊(-1)

expresses the corresponding diagonal Levi element as a product of long-root elements. Every point of the diagonal torus is a product of these coordinate elements. Combining this with the existing Gaussian generation theorem removes its diagonal-torus hypothesis and proves generation by the type-C simple roots alone.

Main results

• TauCeti.GLSymplecticFin.leviHom_diagGL_mulSingle: the rank-one diagonal identity inside the symplectic group.
• TauCeti.GLSymplecticFin.leviHom_diagGL_mem_of_long: opposite long-root subgroups contain the entire diagonal Levi subgroup.
• TauCeti.GLSymplecticFin.eq_top_of_root_subgroups: all standard root subgroups generate the symplectic group over a field.
• TauCeti.GLSymplecticFin.eq_top_of_adjacent_of_long: the positive and negative simple-root families generate the symplectic group over a field.

References

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

theorem TauCeti.GLSymplecticFin.leviHom_diagGL_mulSingle {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (a : Rˣ) : leviHom (diagGL (Pi.mulSingle i a)) = positiveLongRootTransvectionUnit i ↑a * negativeLongRootTransvectionUnit i (-↑a⁻¹) * positiveLongRootTransvectionUnit i ↑a * positiveLongRootTransvectionUnit i (-1) * negativeLongRootTransvectionUnit i 1 * positiveLongRootTransvectionUnit i (-1)

A coordinate diagonal Levi element is a product of six long-root elements. This is the usual rank-one SL₂ identity, embedded in the two symplectic coordinates indexed by i.

theorem TauCeti.GLSymplecticFin.leviHom_diagGL_mem_of_long {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (hpositive : ∀ (i : Fin m) (c : R), positiveLongRootTransvectionUnit i c ∈ H) (hnegative : ∀ (i : Fin m) (c : R), negativeLongRootTransvectionUnit i c ∈ H) (s : Fin m → Rˣ) : leviHom (diagGL s) ∈ H

A subgroup containing both long-root subgroups at every coordinate contains the entire diagonal general-linear Levi subgroup.

theorem TauCeti.GLSymplecticFin.eq_top_of_root_subgroups {m : ℕ} {K : Type u} [Field K] (H : Subgroup ↥(GLSymplecticFin m K)) (hroot : ∀ (root : RootSubgroupIndex m) (c : Multiplicative K), root.hom c ∈ H) : H = ⊤

The standard symplectic root subgroups generate the full symplectic group over a field. The long roots generate the diagonal Levi subgroup, so the diagonal hypothesis in Gaussian generation is automatic.

theorem TauCeti.GLSymplecticFin.eq_top_of_adjacent_of_long {m : ℕ} {K : Type u} [Field K] (H : Subgroup ↥(GLSymplecticFin m K)) (r : Fin m) (hadjacent : ∀ {i j : Fin m} (hij : i ≠ j) (c : K), ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → differenceShortRootUnit hij c ∈ H) (hpositive : ∀ (c : K), positiveLongRootTransvectionUnit r c ∈ H) (hnegative : ∀ (c : K), negativeLongRootTransvectionUnit r c ∈ H) : H = ⊤

The positive and negative simple-root families generate the standard symplectic group over a field. It is enough to contain both orientations of the adjacent difference roots and one positive and negative long-root subgroup. Taking the terminal coordinate gives the Bourbaki simple roots of type C.