Gaussian generation of the symplectic group

Over a field, the standard symplectic group is generated by its root subgroups and split torus. The proof first multiplies a symplectic matrix by an upper unipotent so that its upper-left block is invertible. On that open cell, block Gaussian elimination gives

[A B; C D] = [1 0; C A⁻¹ 1] [A 0; 0 A⁻ᵀ] [1 A⁻¹B; 0 1].

The two off-diagonal blocks are symmetric by the symplectic equations. The outer factors are therefore generated by the long and sum root subgroups. Ordinary matrix elimination expresses the middle general-linear Levi factor using difference roots and diagonal Levi elements.

Main results

• TauCeti.GLSymplecticFin.exists_gaussian_decomposition_of_isUnit_toBlocks₁₁ is the block Gaussian decomposition on the open cell where the upper-left block is invertible.
• TauCeti.GLSymplecticFin.eq_top_of_root_subgroups_of_diagonal proves that all standard root subgroups together with the diagonal Levi subgroup generate the whole symplectic group.
• TauCeti.GLSymplecticFin.eq_top_of_adjacent_of_long_of_diagonal reduces the root hypotheses to both orientations of the adjacent difference roots and one positive and negative long root.

References

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

theorem TauCeti.GLSymplecticFin.exists_gaussian_decomposition_of_isUnit_toBlocks₁₁ {m : ℕ} {R : Type u} [CommRing R] (g : ↥(GLSymplecticFin m R)) (hunit : IsUnit (↑↑((mulEquivGLSymplectic m R) g)).toBlocks₁₁) : ∃ (S : Matrix (Fin m) (Fin m) R) (T : Matrix (Fin m) (Fin m) R) (P : GL (Fin m) R) (hS : S.IsSymm) (hT : T.IsSymm), g = lowerUnipotent S hS * leviHom P * upperUnipotent T hT

A symplectic matrix whose upper-left block is invertible factors as a lower symmetric unipotent, a general-linear Levi element, and an upper symmetric unipotent.

theorem TauCeti.GLSymplecticFin.mem_of_isUnit_toBlocks₁₁ {m : ℕ} {R : Type u} [CommRing R] (H : Subgroup ↥(GLSymplecticFin m R)) (hupper : ∀ (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm), upperUnipotent B hB ∈ H) (hlower : ∀ (C : Matrix (Fin m) (Fin m) R) (hC : C.IsSymm), lowerUnipotent C hC ∈ H) (hlevi : ∀ (A : GL (Fin m) R), leviHom A ∈ H) (g : ↥(GLSymplecticFin m R)) (hunit : IsUnit (↑↑((mulEquivGLSymplectic m R) g)).toBlocks₁₁) : g ∈ H

A symplectic matrix whose upper-left block is invertible belongs to every subgroup containing all upper and lower symmetric unipotents and the general-linear Levi subgroup.

theorem TauCeti.GLSymplecticFin.eq_top_of_root_subgroups_of_diagonal {K : Type u} [Field K] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m K)) (hroot : ∀ (root : RootSubgroupIndex m) (c : Multiplicative K), root.hom c ∈ H) (hdiagonal : ∀ (s : Fin m → Kˣ), leviHom (diagGL s) ∈ H) : H = ⊤

All standard symplectic root subgroups and the diagonal Levi subgroup generate the full symplectic group over a field.

theorem TauCeti.GLSymplecticFin.eq_top_of_adjacent_of_long_of_diagonal {K : Type u} [Field K] {m : ℕ} (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) (hdiagonal : ∀ (s : Fin m → Kˣ), leviHom (diagGL s) ∈ H) : H = ⊤

Both orientations of the adjacent difference roots, one positive and negative long root, and the diagonal Levi subgroup generate the full symplectic group over a field. Choosing the terminal long-root index gives the standard simple-root family of type C.