Generating long and sum roots in the symplectic group

This file develops the root-subgroup generation step for the standard type-C symplectic group beyond its type-A subsystem of difference roots. Over an arbitrary commutative ring, the difference-root subgroups and one pair of opposite long-root subgroups generate every long and sum root subgroup.

The difference-root word

n_{i,j} = x_{eᵢ-eⱼ}(1) x_{eⱼ-eᵢ}(-1) x_{eᵢ-eⱼ}(1)

represents the Weyl reflection exchanging i and j, so conjugation by it carries x_{±2eⱼ}(c) to x_{±2eᵢ}(c). The sum roots are then isolated from the multiply-laced Chevalley commutator relations. In particular, the numbered adjacent difference roots and the final pair of opposite long roots generate every root subgroup in all characteristics, including characteristic two.

Main results

• TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit_mem_of_difference_of_long and its negative analogue transport one long-root subgroup to a target index by Weyl conjugation.
• TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_apply_mem_of_difference_of_long packages the result for every standard symplectic root subgroup.
• TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_apply_mem_of_adjacent_of_long reduces the hypotheses further to the positive and negative simple-root families.

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 every root subgroup required for the reverse inclusion of the full-weight type-C carrier in the standard symplectic group. Removing the former invertibility-of-two hypothesis is necessary for the characteristic-two type-C branch consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

theorem TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit_mem_of_difference_of_long {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (r i : Fin m) (hforward : ∀ (hir : i ≠ r), differenceShortRootUnit hir 1 ∈ H) (hbackward : ∀ (hir : i ≠ r), differenceShortRootUnit ⋯ (-1) ∈ H) (c : R) (hpivot : positiveLongRootTransvectionUnit r c ∈ H) : positiveLongRootTransvectionUnit i c ∈ H

If a subgroup contains the two difference-root elements forming the Weyl word from r to i and the positive long-root element at r, then it contains the corresponding positive long-root element at i.

theorem TauCeti.GLSymplecticFin.negativeLongRootTransvectionUnit_mem_of_difference_of_long {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (r i : Fin m) (hforward : ∀ (hir : i ≠ r), differenceShortRootUnit hir 1 ∈ H) (hbackward : ∀ (hir : i ≠ r), differenceShortRootUnit ⋯ (-1) ∈ H) (c : R) (hpivot : negativeLongRootTransvectionUnit r c ∈ H) : negativeLongRootTransvectionUnit i c ∈ H

If a subgroup contains the two difference-root elements forming the Weyl word from r to i and the negative long-root element at r, then it contains the corresponding negative long-root element at i.

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_apply_mem_of_difference_of_long {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (r : Fin m) (hdifference : ∀ {i j : Fin m} (hij : i ≠ j) (c : R), differenceShortRootUnit hij c ∈ H) (hpositive : ∀ (c : R), positiveLongRootTransvectionUnit r c ∈ H) (hnegative : ∀ (c : R), negativeLongRootTransvectionUnit r c ∈ H) (root : RootSubgroupIndex m) (c : Multiplicative R) : root.hom c ∈ H

Difference roots and one opposite pair of long-root subgroups generate every symplectic root subgroup. More precisely, if H contains every difference-root element and both long-root subgroups at one index, then the value of every root one-parameter subgroup lies in H.

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_apply_mem_of_adjacent_of_long {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (r : Fin m) (hadjacent : ∀ {i j : Fin m} (hij : i ≠ j) (c : R), ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → differenceShortRootUnit hij c ∈ H) (hpositive : ∀ (c : R), positiveLongRootTransvectionUnit r c ∈ H) (hnegative : ∀ (c : R), negativeLongRootTransvectionUnit r c ∈ H) (root : RootSubgroupIndex m) (c : Multiplicative R) : root.hom c ∈ H

The positive and negative simple-root families generate every standard symplectic root subgroup. It is enough for H to contain the two orientations of every adjacent difference root and one pair of opposite long-root subgroups. This formulation matches the numbered simple roots of type C and holds over every commutative ring.