Chevalley relations in the toral Kostant group scheme

The represented root subgroups first generate a closed group scheme inside GLₙ, and that root-generated carrier includes as a closed subgroup of the larger carrier generated jointly by the root subgroups and the represented weight torus. This file transports the intrinsic Chevalley relations from the root-generated carrier through that inclusion. Consequently the root subgroups of the toral carrier satisfy the same commuting, class-two, multiply-laced, and type-G₂ relations on points over every commutative ring.

The transport uses TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_comp_kostantGeneratedToToral; no relation is reproved at matrix level. The resulting statements are on kostantRootSubgroupToToral, the root-subgroup interface of the carrier used by the Chevalley--Demazure construction.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.commute_kostantRootSubgroupToToral: commuting root vectors give commuting points of the toral group scheme.
• TauCeti.UniversalEnvelopingAlgebra. commutatorElement_kostantRootSubgroupToToral_of_lie_eq: the class-two Chevalley relation.
• TauCeti.UniversalEnvelopingAlgebra. commutatorElement_kostantRootSubgroupToToral_of_lie_lie_eq: the multiply-laced relation.
• TauCeti.UniversalEnvelopingAlgebra. kostantRootSubgroupToToral_mul_of_lie_eq_three_nsmul: the type-G₂ relation.

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.

This supplies the Chevalley commutator interface for the toral carrier in Layer 9 of the ReductiveGroups roadmap. That carrier and its root subgroups are consumed by milestone L0 of the CFSGStatement roadmap.

theorem TauCeti.UniversalEnvelopingAlgebra.commute_kostantRootSubgroupToToral {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (wt : Fin n → κ → ℤ) (A : Type) [CommRing A] {i j : I} (hij : ⁅e i, e j⁆ = 0) (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : Commute (CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom) (CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToToral e h ρ M hM hnil b wt j).hom.hom)

Represented Kostant root subgroups attached to commuting root vectors commute as points of the toral group scheme over every commutative value ring.

theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupToToral_of_lie_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (wt : Fin n → κ → ℤ) (A : Type) [CommRing A] {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) (p q r : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) (hr : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) r) = ↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q))) : ⁅CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom, CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToToral e h ρ M hM hnil b wt j).hom.hom⁆ = CategoryTheory.CategoryStruct.comp r (kostantRootSubgroupToToral e h ρ M hM hnil b wt k).hom.hom

The class-two Chevalley commutator relation inside the toral Kostant group scheme. Suppose ⁅eᵢ, eⱼ⁆ = c • eₖ, with eₖ commuting with both input vectors. If the additive parameter of r is c times the product of those of p and q, then the commutator of the factored i- and j-root points is the factored k-root point at r.

theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupToToral_of_lie_lie_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (wt : Fin n → κ → ℤ) (A : Type) [CommRing A] {i j k l : I} {c d : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hiij : ⁅e i, ⁅e i, e j⁆⁆ = (2 * d) • e l) (hil : ⁅e i, e l⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hjl : ⁅e j, e l⁆ = 0) (hkl : ⁅e k, e l⁆ = 0) (p q r s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) (hr : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) r) = ↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q))) (hs : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) s) = ↑d * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q))) : ⁅CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom, CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToToral e h ρ M hM hnil b wt j).hom.hom⁆ = CategoryTheory.CategoryStruct.comp r (kostantRootSubgroupToToral e h ρ M hM hnil b wt k).hom.hom * CategoryTheory.CategoryStruct.comp s (kostantRootSubgroupToToral e h ρ M hM hnil b wt l).hom.hom

The multiply-laced Chevalley commutator relation inside the toral Kostant group scheme. The indices i, j, k, l correspond to α, β, α + β, 2α + β. If r and s have parameters c t u and d t² u, then the commutator of the factored input points is the product of the two factored output points.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToToral_mul_of_lie_eq_three_nsmul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (wt : Fin n → κ → ℤ) (A : Type) [CommRing A] {i j k l m o : I} {c d a b' : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : c • ⁅e i, e k⁆ = (2 * d) • e l) (hil : d • ⁅e i, e l⁆ = (3 * a) • e m) (hlk : (d * c) • ⁅e l, e k⁆ = (3 * b') • e o) (him : ⁅e i, e m⁆ = 0) (hio : ⁅e i, e o⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hlm : ⁅e l, e m⁆ = 0) (hko : ⁅e k, e o⁆ = 0) (hlo : ⁅e l, e o⁆ = 0) (hmo : ⁅e m, e o⁆ = 0) (f g p q r s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) (hp : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) = ↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))) (hq : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q) = ↑d * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))) (hr : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) r) = ↑a * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))) (hs : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) s) = ↑b' * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g) ^ 2)) : CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom * CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToToral e h ρ M hM hnil b wt j).hom.hom = CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToToral e h ρ M hM hnil b wt j).hom.hom * CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToToral e h ρ M hM hnil b wt k).hom.hom * CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToToral e h ρ M hM hnil b wt l).hom.hom * CategoryTheory.CategoryStruct.comp r (kostantRootSubgroupToToral e h ρ M hM hnil b wt m).hom.hom * CategoryTheory.CategoryStruct.comp s (kostantRootSubgroupToToral e h ρ M hM hnil b wt o).hom.hom * CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom

The type-G₂ Chevalley product relation inside the toral Kostant group scheme. The indices i, j, k, l, m, o correspond to α, β, α + β, 2α + β, 3α + β, 3α + 2β. The four supplied output points have parameters c t u, d t² u, a t³ u, and b t³ u².