Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Torus.Coroot

Coroot values in the elementary group, and when the weight torus is redundant #

The points of a Kostant carrier over a value ring A are generated by two families: the root subgroups xᵢ(t), generating the elementary group TauCeti.UniversalEnvelopingAlgebra.kostantElementarySubgroup, and the split weight torus t(s). This file shows that the second family is often already contained in the first, so that the torus contributes no new points.

The mechanism is Chevalley's, and it needs no new computation inside the sl₂ triple. Write n = xᵢ(1) xⱼ(-1) xᵢ(1) for the Weyl representative of a root pair (eᵢ, eⱼ) with Cartan index c, and α for the weight of eᵢ. Conjugation by a torus point rescales the parameter of each root subgroup, so n lies in the elementary group and the elementary group is stable under that conjugation; hence

t(s) t(s_α s)⁻¹ = t(s) n t(s)⁻¹ n⁻¹

lies in the elementary group. The left-hand side is a torus point again, and a very particular one: the reflection s_α divides the c-th coordinate of s by the value α(s) and leaves the others alone, so the product above is the point supported at c with value α(s). Under the displayed sl₂-triple hypothesis, the c-th coordinate cocharacter is Chevalley's coroot cocharacter, and the identity puts its value at α(s) in the elementary group for every s.

What is left is a question about the integers alone: which values u arise as α(s)? Writing α in the coordinates of the designated Cartan vectors, α(s) = ∏ⱼ s(j) ^ α(j), so every unit arises as soon as the integers α(j) are setwise coprime. For a simple root of an irreducible finite Dynkin diagram those integers are its row of the Cartan matrix, which is coprime precisely when it contains an odd entry: equivalently, an off-diagonal -1 or -3. The rows that are not coprime are the rank-one row (2) and the long-simple-root rows of B₂ and Cₙ; the long row (-3, 2) of G₂ has no -1 but is nevertheless coprime. When the condition holds at every Cartan index the whole torus lies in the elementary group, and the Borel-type join of the torus with all root subgroups collapses to the elementary group.

Nothing here identifies the elementary group with the points of the toral closure group scheme, which is a separate statement that this file does not use or prove: the comparison is between two subgroups of Aut_A(A ⊗[ℤ] M), both generated by named elements.

The cocharacter supported at one coordinate, TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter, and the identity TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_mul_inv_weylReflectTorusPoint expressing the quotient displayed above as one of its values, both belong to the torus itself and are imported from TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/Torus/Basic.lean.

Main results #

References #

Coroot values in the elementary group #

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter_torusCharacter_mem_kostantElementarySubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] [DecidableEq κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (rt : ι → κ → ℤ) (hrt : ∀ (i : ι) (j : κ), ⁅h j, e i⁆ = ↑(rt i j) • e i) {i j : ι} {c : κ} (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hopp : rt j = -rt i) (A : CommAlgCat ℤ) (s : κ → (↑A)ˣ) :
(kostantCoordinateCocharacter M b wt (↑A) c) (torusCharacter s (rt i)) ∈ kostantElementarySubgroup e h ρ M hM hnil A

A coroot element at a value of the root lies in the elementary group. For every torus point s, the coroot element at the Cartan index c with value α(s) is the commutator t(s) n t(s)⁻¹ n⁻¹ of s with the Weyl representative n of the root pair, and both factors are elementary: the torus normalizes the elementary group, which contains n.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter_mem_kostantElementarySubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] [DecidableEq κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (rt : ι → κ → ℤ) (hrt : ∀ (i : ι) (j : κ), ⁅h j, e i⁆ = ↑(rt i j) • e i) {i j : ι} {c : κ} (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hopp : rt j = -rt i) {m : κ → ℤ} (hm : ∑ j' : κ, rt i j' * m j' = 1) (A : CommAlgCat ℤ) (u : (↑A)ˣ) :
(kostantCoordinateCocharacter M b wt (↑A) c) u ∈ kostantElementarySubgroup e h ρ M hM hnil A

A unimodular root puts every coroot element in the elementary group. If the coordinates of the root rt i have a ℤ-linear combination equal to one, then every unit is a value α(s), so the previous result reaches the whole coroot cocharacter.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubgroup_le_kostantElementarySubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (rt : ι → κ → ℤ) (hrt : ∀ (i : ι) (j : κ), ⁅h j, e i⁆ = ↑(rt i j) • e i) (raise lower : κ → ι) (hT : ∀ (c : κ), IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (raise c)))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (lower c))))) (hopp : ∀ (c : κ), rt (lower c) = -rt (raise c)) (m : κ → κ → ℤ) (hm : ∀ (c : κ), ∑ j' : κ, rt (raise c) j' * m c j' = 1) (A : CommAlgCat ℤ) :
kostantTorusSubgroup M b wt ↑A ≤ kostantElementarySubgroup e h ρ M hM hnil A

The weight torus lies in the elementary group. A torus point is the product over the Cartan indices of its coroot elements, so a unimodular root pair at every index puts the whole torus inside the group generated by the root subgroups.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup_univ_eq_kostantElementarySubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (rt : ι → κ → ℤ) (hrt : ∀ (i : ι) (j : κ), ⁅h j, e i⁆ = ↑(rt i j) • e i) (raise lower : κ → ι) (hT : ∀ (c : κ), IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (raise c)))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (lower c))))) (hopp : ∀ (c : κ), rt (lower c) = -rt (raise c)) (m : κ → κ → ℤ) (hm : ∀ (c : κ), ∑ j' : κ, rt (raise c) j' * m c j' = 1) (A : CommAlgCat ℤ) :
kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt Set.univ A = kostantElementarySubgroup e h ρ M hM hnil A

The Borel-type join of the torus with every root subgroup is the elementary group. With a unimodular root pair at every Cartan index the torus is redundant, so adjoining it to the root subgroups adds nothing.