Chevalley relations for represented Kostant root subgroups

A Kostant-stable integral lattice and a finite basis represent each divided-power root action by an affine group-scheme morphism xᵢ : 𝔾ₐ → GLₙ. This file connects those represented morphisms to the Chevalley relations already proved for the underlying divided-power actions.

If two distinguished root vectors commute, their represented root-subgroup values commute. If

⁅eᵢ, eⱼ⁆ = c eₖ,   ⁅eᵢ, eₖ⁆ = 0,   ⁅eⱼ, eₖ⁆ = 0,

then the canonical commutator relation is

⁅xᵢ(t), xⱼ(u)⁆ = xₖ(c t u).

This file provides the relations in any finite integral basis. Their scheme-valued counterparts are in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.Relations.Basic.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.commute_kostantRootSubgroupMatrix: the commuting relation in an integral basis.
• TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupMatrix_of_lie_eq: the class-two relation in an integral basis.
• TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupMatrix_of_lie_eq': the class-two relation with the third point written out.

References

• R. W. Carter, Simple Groups of Lie Type, Theorem 5.2.2.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Sections 26--27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

theorem TauCeti.UniversalEnvelopingAlgebra.commute_kostantRootSubgroupMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) {A : Type u_2} [CommRing A] {η : Type u_3} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {i j : I} (hij : ⁅e i, e j⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (f g : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : Commute ((kostantRootSubgroupMatrix e h ρ M hM i hi b) f) ((kostantRootSubgroupMatrix e h ρ M hM j hj b) g)

Represented Kostant root subgroups attached to commuting root vectors commute in every integral basis.

theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupMatrix_of_lie_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) {A : Type u_2} [CommRing A] {η : Type u_3} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {i j k : I} {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (f g z : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (hz : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv z) = ↑c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) : ⁅(kostantRootSubgroupMatrix e h ρ M hM i hi b) f, (kostantRootSubgroupMatrix e h ρ M hM j hj b) g⁆ = (kostantRootSubgroupMatrix e h ρ M hM k hk b) z

The class-two Chevalley commutator relation in an integral basis. The matrix commutator of the first two represented root subgroups is the third at parameter c t u.

theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupMatrix_of_lie_eq' {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) {A : Type u_2} [CommRing A] {η : Type u_3} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {i j k : I} {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (f g : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : ⁅(kostantRootSubgroupMatrix e h ρ M hM i hi b) f, (kostantRootSubgroupMatrix e h ρ M hM j hj b) g⁆ = (kostantRootSubgroupMatrix e h ρ M hM k hk b) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g)))))

The class-two Chevalley commutator relation in an integral basis with the third 𝔾ₐ-point written out at parameter c times the product of the parameters of f and g.