Commuting simple-root subgroups of the Geck carrier

The pinned raising and lowering root subgroups of the Geck carrier satisfy the zero-pairing Chevalley relation over every commutative ring. When two distinct Bourbaki nodes have zero Cartan pairing, both raising subgroups commute, both lowering subgroups commute, and each raising subgroup commutes with the other node's lowering subgroup. The last relation holds for any distinct nodes.

The statements concern the pinned Serre generators and their Kostant root-subgroup points, both in the matrix model and as scheme-valued points of the Geck carrier. These relations are used in the presentation of the pinned split group by its simple-root subgroups; relations among nonorthogonal roots require the higher root-string formulas.

Main results

• TauCeti.DynkinType.commute_geckSimpleRaisingPoints and its lowering and mixed-sign variants give the relations in the represented matrix group.
• TauCeti.DynkinType.commute_geckSimpleRaisingSchemePoints and its lowering and mixed-sign variants give the same relations for the root-subgroup morphisms of the Geck group scheme.

References

• R. Steinberg, Lectures on Chevalley Groups, §3.
• R. W. Carter, Simple Groups of Lie Type, §5.2.

@[simp]

theorem TauCeti.DynkinType.lie_geckSimpleRaising_eq_zero (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : t.cartanMatrix i j = 0) : ⁅(t.lieBasis ht).e i, (t.lieBasis ht).e j⁆ = 0

The pinned raising generators at nodes with zero Cartan pairing have zero Lie bracket.

@[simp]

theorem TauCeti.DynkinType.lie_geckSimpleLowering_eq_zero (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : t.cartanMatrix i j = 0) : ⁅(t.lieBasis ht).f i, (t.lieBasis ht).f j⁆ = 0

The pinned lowering generators at nodes with zero Cartan pairing have zero Lie bracket.

@[simp]

theorem TauCeti.DynkinType.lie_geckSimpleRaising_lowering_eq_zero (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : i ≠ j) : ⁅(t.lieBasis ht).e i, (t.lieBasis ht).f j⁆ = 0

Raising at one node and lowering at a distinct node have zero Lie bracket.

theorem TauCeti.DynkinType.commute_geckRootSubgroupPoints_of_lie_eq_zero (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank ⊕ Fin t.rank) (hij : ⁅(t.lieBasis ht).rootGenerator i, (t.lieBasis ht).rootGenerator j⁆ = 0) (A : Type v) [CommRing A] (u w : Multiplicative A) : Commute ((t.geckRootSubgroupPoints ht i A) u) ((t.geckRootSubgroupPoints ht j A) w)

Two numbered Geck root-subgroup points commute when their pinned Lie generators commute.

theorem TauCeti.DynkinType.commute_geckSimpleRaisingPoints (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : t.cartanMatrix i j = 0) (A : Type v) [CommRing A] (u w : Multiplicative A) : Commute ((t.geckRootSubgroupPoints ht (Sum.inl i) A) u) ((t.geckRootSubgroupPoints ht (Sum.inl j) A) w)

Raising subgroups at orthogonal simple roots commute over every commutative ring.

theorem TauCeti.DynkinType.commute_geckSimpleLoweringPoints (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : t.cartanMatrix i j = 0) (A : Type v) [CommRing A] (u w : Multiplicative A) : Commute ((t.geckRootSubgroupPoints ht (Sum.inr i) A) u) ((t.geckRootSubgroupPoints ht (Sum.inr j) A) w)

Lowering subgroups at orthogonal simple roots commute over every commutative ring.

theorem TauCeti.DynkinType.commute_geckSimpleRaising_loweringPoints (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : i ≠ j) (A : Type v) [CommRing A] (u w : Multiplicative A) : Commute ((t.geckRootSubgroupPoints ht (Sum.inl i) A) u) ((t.geckRootSubgroupPoints ht (Sum.inr j) A) w)

The raising subgroup at one node commutes with the lowering subgroup at another node.

theorem TauCeti.DynkinType.commute_geckSimpleLowering_raisingPoints (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : i ≠ j) (A : Type v) [CommRing A] (u w : Multiplicative A) : Commute ((t.geckRootSubgroupPoints ht (Sum.inr i) A) u) ((t.geckRootSubgroupPoints ht (Sum.inl j) A) w)

The lowering subgroup at one node commutes with the raising subgroup at another node.

Relations on scheme-valued points

theorem TauCeti.DynkinType.commute_geckRootSubgroupSchemePoints_of_lie_eq_zero (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank ⊕ Fin t.rank) (hij : ⁅(t.lieBasis ht).rootGenerator i, (t.lieBasis ht).rootGenerator j⁆ = 0) (A : Type) [CommRing A] (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : Commute (CategoryTheory.CategoryStruct.comp p (t.geckRootSubgroup ht i).hom.hom) (CategoryTheory.CategoryStruct.comp q (t.geckRootSubgroup ht j).hom.hom)

Two numbered Geck root-subgroup morphisms give commuting scheme-valued points whenever their pinned Lie generators commute.

theorem TauCeti.DynkinType.commute_geckSimpleRaisingSchemePoints (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : t.cartanMatrix i j = 0) (A : Type) [CommRing A] (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : Commute (CategoryTheory.CategoryStruct.comp p (t.geckRootSubgroup ht (Sum.inl i)).hom.hom) (CategoryTheory.CategoryStruct.comp q (t.geckRootSubgroup ht (Sum.inl j)).hom.hom)

Raising root-subgroup morphisms at orthogonal simple roots give commuting scheme-valued points over every commutative ring.

theorem TauCeti.DynkinType.commute_geckSimpleLoweringSchemePoints (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : t.cartanMatrix i j = 0) (A : Type) [CommRing A] (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : Commute (CategoryTheory.CategoryStruct.comp p (t.geckRootSubgroup ht (Sum.inr i)).hom.hom) (CategoryTheory.CategoryStruct.comp q (t.geckRootSubgroup ht (Sum.inr j)).hom.hom)

Lowering root-subgroup morphisms at orthogonal simple roots give commuting scheme-valued points over every commutative ring.

theorem TauCeti.DynkinType.commute_geckSimpleRaising_loweringSchemePoints (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : i ≠ j) (A : Type) [CommRing A] (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : Commute (CategoryTheory.CategoryStruct.comp p (t.geckRootSubgroup ht (Sum.inl i)).hom.hom) (CategoryTheory.CategoryStruct.comp q (t.geckRootSubgroup ht (Sum.inr j)).hom.hom)

Raising at one node and lowering at a distinct node give commuting scheme-valued points of the Geck carrier.

theorem TauCeti.DynkinType.commute_geckSimpleLowering_raisingSchemePoints (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) (hij : i ≠ j) (A : Type) [CommRing A] (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : Commute (CategoryTheory.CategoryStruct.comp p (t.geckRootSubgroup ht (Sum.inr i)).hom.hom) (CategoryTheory.CategoryStruct.comp q (t.geckRootSubgroup ht (Sum.inl j)).hom.hom)

Lowering at one node and raising at a distinct node give commuting scheme-valued points of the Geck carrier.