The pinning equation in the toral Kostant group scheme

The toral Kostant group scheme is the closed subgroup scheme of GLₙ generated jointly by a represented split torus and a family of represented root subgroups. Both kinds of generators factor through that carrier, but the equation relating them was previously available only after mapping back into GL_n:

t(s) x_i(u) t(s)⁻¹ = x_i(α(s) u).

This file proves the equation intrinsically in the toral carrier, on points over every commutative ring. The proof uses the closed immersion into GL_n only to reflect equality. Its input is the mathematical weight equation [h_j, e_i] = α_j e_i; no compatibility is added as an assumption on the constructed group scheme.

Main results

• TauCeti.UniversalEnvelopingAlgebra. kostantWeightTorusToToral_mul_kostantRootSubgroupToToral: the intertwining form t(s) x_i(u) = x_i(α(s) u) t(s).
• TauCeti.UniversalEnvelopingAlgebra. kostantWeightTorusToToral_conj_kostantRootSubgroupToToral: the conjugation form of the pinning equation.
• TauCeti.UniversalEnvelopingAlgebra. kostantWeightTorusToToral_conj_kostantRootSubgroupToToralParam: the same equation with its root-subgroup parameter read directly in the value ring.

References

This is the torus--root-subgroup compatibility equation intended for the future pinning of the Chevalley--Demazure group scheme; see J. E. Humphreys, Linear Algebraic Groups, Section 26, and R. W. Carter, Simple Groups of Lie Type, Sections 4.4 and 7.1. It advances the Pinnings and Root subgroup maps targets of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of the CFSGStatement roadmap.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToToral_mul_kostantRootSubgroupToToral {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : Type) [CommRing A] {i : I} {α : κ → ℤ} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ κ).X) (u v : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) (hv : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) v) = ↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) α) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) u)) : CategoryTheory.CategoryStruct.comp s (kostantWeightTorusToToral e h ρ M hM hnil b wt).hom.hom * CategoryTheory.CategoryStruct.comp u (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom = CategoryTheory.CategoryStruct.comp v (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom * CategoryTheory.CategoryStruct.comp s (kostantWeightTorusToToral e h ρ M hM hnil b wt).hom.hom

The pinning equation in the toral Kostant group scheme, in intertwining form. If e_i has Cartan weight α, then a torus point s and root-subgroup parameters u, v satisfying v = α(s) u obey t(s) x_i(u) = x_i(v) t(s) inside the toral carrier.

The statement is on points over an arbitrary commutative ring. The parameter equation is stated through the canonical scheme-point coordinates of the split torus and additive group.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToToral_conj_kostantRootSubgroupToToral {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : Type) [CommRing A] {i : I} {α : κ → ℤ} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ κ).X) (u : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : CategoryTheory.CategoryStruct.comp s (kostantWeightTorusToToral e h ρ M hM hnil b wt).hom.hom * CategoryTheory.CategoryStruct.comp u (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom * (CategoryTheory.CategoryStruct.comp s (kostantWeightTorusToToral e h ρ M hM hnil b wt).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) α) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) u)))) (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom

The pinning equation in the toral Kostant group scheme. Conjugation by the torus point t(s) sends the ith root-subgroup point with parameter u to the same root subgroup with parameter α(s) u, where α is the Cartan weight of e_i.

This is the intrinsic equation later diagram automorphisms and Steinberg maps are normalized against; it no longer mentions the embedding of the constructed carrier into GL_n.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToToral_conj_kostantRootSubgroupToToralParam {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : Type) [CommRing A] {i : I} {α : κ → ℤ} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ κ).X) (u : A) : CategoryTheory.CategoryStruct.comp s (kostantWeightTorusToToral e h ρ M hM hnil b wt).hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd u))) (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom * (CategoryTheory.CategoryStruct.comp s (kostantWeightTorusToToral e h ρ M hM hnil b wt).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) α) * u))) (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom

The pinning equation with the root-subgroup parameter read in the value ring. Conjugation by t(s) sends x_i(u) to x_i(α(s) u) inside the toral carrier.