Generating the sum-root subgroups of the symplectic group

The standard type-C_m root system has short roots eᵢ - eⱼ, eᵢ + eⱼ, and -eᵢ - eⱼ, together with the long roots ±2eᵢ. This file uses the multiply-laced Chevalley relations to recover the two sum-root families from the difference-root and long-root families. For distinct i and j, specializing the positive relation at parameter one gives

⁅x_{eᵢ-eⱼ}(1), x_{2eⱼ}(c)⁆ = x_{eᵢ+eⱼ}(c) x_{2eᵢ}(c),

and the negative relation at -c gives the corresponding formula for -eᵢ-eⱼ. Thus a subgroup containing every difference-root and long-root element contains every root element of the standard symplectic realization. The argument uses no division, so it works over every commutative ring, including characteristic two.

Main results

• TauCeti.GLSymplecticFin.positiveSumShortRootUnit_mem_of_difference_long: a positive sum-root element belongs to a subgroup containing the three elements in the specialized commutator relation.
• TauCeti.GLSymplecticFin.negativeSumShortRootUnit_mem_of_difference_long: the parallel negative result.
• TauCeti.GLSymplecticFin.rootSubgroupHom_mem_of_difference_long: difference-root and long-root families generate every root family.

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 is the sum-root generation step needed to identify the explicit full-weight type-C carrier with the standard symplectic group on field-valued points. That identification is consumed by the C_n(q) branch of milestone L0 in TauCetiRoadmap/CFSGStatement/README.md.

theorem TauCeti.GLSymplecticFin.positiveSumShortRootUnit_mem_of_difference_long {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (H : Subgroup ↥(GLSymplecticFin m R)) (hij : i ≠ j) (c : R) (hdifference : differenceShortRootUnit hij 1 ∈ H) (hsource : positiveLongRootTransvectionUnit j c ∈ H) (htarget : positiveLongRootTransvectionUnit i c ∈ H) : positiveSumShortRootUnit hij c ∈ H

A positive sum-root element lies in any subgroup containing the parameter-one difference-root element and the two positive long-root elements occurring in its Chevalley commutator formula.

theorem TauCeti.GLSymplecticFin.negativeSumShortRootUnit_mem_of_difference_long {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (H : Subgroup ↥(GLSymplecticFin m R)) (hij : i ≠ j) (c : R) (hdifference : differenceShortRootUnit hij 1 ∈ H) (hsource : negativeLongRootTransvectionUnit i (-c) ∈ H) (htarget : negativeLongRootTransvectionUnit j (-c) ∈ H) : negativeSumShortRootUnit hij c ∈ H

A negative sum-root element lies in any subgroup containing the parameter-one difference-root element and the two negative long-root elements occurring in its Chevalley commutator formula.

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

If a subgroup of the standard symplectic group contains every difference-root element and every positive and negative long-root element, then it contains every standard root-subgroup element. This is valid over an arbitrary commutative ring.