Commuting simple-root subgroups of the type-E₇ minuscule carrier

The numbered positive and negative simple-root subgroups of the integral minuscule carrier satisfy the commuting Chevalley relations. Two roots of the same sign commute when their nodes are not joined in the Dynkin diagram, and roots of opposite signs commute at distinct nodes. These are equalities in the carrier's group of points over every commutative ring, including rings of positive characteristic.

Together these give the zero-commutator cases of the pinned Chevalley relations for the E₇ carrier. They allow the numbered root-subgroup points to be reordered at nonadjacent nodes or at distinct nodes with opposite signs.

References

• Formalization adapted: TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.SimpleRootRelations.
• R. W. Carter, Simple Groups of Lie Type, Theorem 5.2.2.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§25–26.

theorem TauCeti.E7Minuscule.commute_rootSubgroupPoints_inl_inl {i j : Fin 7} (hij : CartanMatrix.E 7 i j = 0) (A : Type u) [CommRing A] (s t : Multiplicative A) : Commute ((rootSubgroupPoints (Sum.inl i) A) s) ((rootSubgroupPoints (Sum.inl j) A) t)

Positive numbered simple-root subgroups at nonadjacent nodes commute over every commutative ring.

theorem TauCeti.E7Minuscule.commute_rootSubgroupPoints_inr_inr {i j : Fin 7} (hij : CartanMatrix.E 7 i j = 0) (A : Type u) [CommRing A] (s t : Multiplicative A) : Commute ((rootSubgroupPoints (Sum.inr i) A) s) ((rootSubgroupPoints (Sum.inr j) A) t)

Negative numbered simple-root subgroups at nonadjacent nodes commute over every commutative ring.

theorem TauCeti.E7Minuscule.commute_rootSubgroupPoints_inl_inr {i j : Fin 7} (hij : i ≠ j) (A : Type u) [CommRing A] (s t : Multiplicative A) : Commute ((rootSubgroupPoints (Sum.inl i) A) s) ((rootSubgroupPoints (Sum.inr j) A) t)

A positive and a negative numbered simple-root subgroup at distinct nodes commute over every commutative ring.

theorem TauCeti.E7Minuscule.commute_rootSubgroupPoints_inr_inl {i j : Fin 7} (hij : i ≠ j) (A : Type u) [CommRing A] (s t : Multiplicative A) : Commute ((rootSubgroupPoints (Sum.inr i) A) s) ((rootSubgroupPoints (Sum.inl j) A) t)

A negative and a positive numbered simple-root subgroup at distinct nodes commute over every commutative ring.