Chevalley relations for the root subgroups of the special linear group

For distinct indices, TauCeti.SpecialLinear.rootSubgroupPoints identifies an additive-group point of parameter c with the determinant-one elementary matrix

xᵢⱼ(c) = 1 + c Eᵢⱼ.

This file transports the type-A Chevalley commutator relations from elementary matrices to the functor of points of SLₙ. If two index pairs do not chain, their special-linear root-subgroup values commute. For three distinct indices, the chaining relation is

⁅xᵢⱼ(c), xⱼₗ(d)⁆ = xᵢₗ(cd).

The product cd is multiplication in the value algebra, not the convolution product on 𝔾ₐ(A), which corresponds to addition. The additive-group operation TauCeti.AdditiveGroup.gaPointParamMul packages this distinction and is natural in the value algebra.

On scheme-valued points, composing with the special-linear root subgroup morphism satisfies the corresponding commutation and commutator relations. The scheme-level parameter product is TauCeti.AdditiveGroup.gaSchemePointParamMul, the scheme-point counterpart of gaPointParamMul.

This file supplies the commutator-relations part of the pinned Chevalley–Demazure interface from Layer 9 of the ReductiveGroups roadmap for the worked example SLₙ over an arbitrary commutative base ring.

Main declarations

• TauCeti.SpecialLinear.commute_rootSubgroupPoints: root subgroups at non-chaining index pairs commute in SLₙ(A).
• TauCeti.SpecialLinear.commutatorElement_rootSubgroupPoints: the type-A Chevalley commutator relation on algebra-valued points of SLₙ.
• TauCeti.SpecialLinear.commute_schemePointsMulEquiv_rootSubgroup: commutation on scheme-valued points of SLₙ.
• TauCeti.SpecialLinear.commutatorElement_schemePointsMulEquiv_rootSubgroup: the type-A Chevalley commutator relation on scheme-valued points of SLₙ.

References

• The formal development in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.ChevalleyRelations, adapted here from GLₙ to SLₙ.
• R. W. Carter, Simple Groups of Lie Type (1972), §11.3.
• J. E. Humphreys, Linear Algebraic Groups (1975), §26.3.
• J. S. Milne, Algebraic Groups (2017), §21.

theorem TauCeti.SpecialLinear.commute_rootSubgroupPoints {R : Type u} [CommRing R] {A : Type w} [CommRing A] [Algebra R A] {N : ℕ} {i j k l : Fin N} (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (f g : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) : Commute ((rootSubgroupPoints hij) f) ((rootSubgroupPoints hkl) g)

Root-subgroup values at two non-chaining index pairs commute in SLₙ(A).

The hypotheses j ≠ k and l ≠ i state that the sum of the roots εᵢ - εⱼ and εₖ - εₗ is neither a root nor zero.

theorem TauCeti.SpecialLinear.commutatorElement_rootSubgroupPoints {R : Type u} [CommRing R] {A : Type w} [CommRing A] [Algebra R A] {N : ℕ} {i j l : Fin N} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) (f g : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) : ⁅(rootSubgroupPoints hij) f, (rootSubgroupPoints hjl) g⁆ = (rootSubgroupPoints hil) (AdditiveGroup.gaPointParamMul f g)

The type-A Chevalley commutator relation on algebra-valued points of SLₙ. For three distinct indices,

⁅xᵢⱼ(c), xⱼₗ(d)⁆ = xᵢₗ(cd).

The point on the right has parameter cd in the value algebra, as recorded by AdditiveGroup.gaPointParamMul.

theorem TauCeti.SpecialLinear.commute_schemePointsMulEquiv_rootSubgroup {R : Type u} [CommRing R] {N : ℕ} {i j k l : Fin N} (A : Type u) [CommRing A] [Algebra R A] (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (AdditiveGroup.groupScheme R).X) : Commute ((schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp p (rootSubgroup hij).hom.hom)) ((schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp q (rootSubgroup hkl).hom.hom))

On scheme-valued points of SLₙ, root subgroups at non-chaining index pairs commute.

theorem TauCeti.SpecialLinear.commutatorElement_schemePointsMulEquiv_rootSubgroup {R : Type u} [CommRing R] {N : ℕ} {i j l : Fin N} (A : Type u) [CommRing A] [Algebra R A] (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (AdditiveGroup.groupScheme R).X) : ⁅(schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp p (rootSubgroup hij).hom.hom), (schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp q (rootSubgroup hjl).hom.hom)⁆ = (schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp (AdditiveGroup.gaSchemePointParamMul A p q) (rootSubgroup hil).hom.hom)

The type-A Chevalley commutator relation on scheme-valued points of SLₙ. The root-subgroup point on the right has parameter cd, the product in the value algebra A of the parameters of p and q; this is not their convolution product, which corresponds to addition.