The Weyl element normalises the split torus

Let U_ℤ = kostantForm e h act on a rational vector space V through ρ and preserve an additive subgroup M ≤ V, presented in a weight basis, and let eᵢ, eⱼ be distinguished root vectors whose images span, together with the distinguished Cartan vector h c, an sl₂ triple. The two halves of the pinning built so far are the split torus t(s) of TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/Torus/Basic.lean, which acts on a weight vector of weight μ by the character value μ(s), and the Weyl element n = x_i(1) x_j(-1) x_i(1) of TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/Weyl/Basic.lean, which interchanges the root subgroups of α and -α. This file proves the remaining pinning relation between them: n normalises the torus, and conjugation by it is the reflection s_α.

The mechanism is the coreflection formula for the Weyl element, TauCeti.inv_weylUnit_conj_of_lie_eq_smul, which says that an operator acting on the raising and lowering elements by the opposite scalars c and -c is conjugated to y - c • H. Applied to the designated Cartan operators ρ(hⱼ), with α the weight of eᵢ, it gives

n⁻¹ ρ(hⱼ) n = ρ(hⱼ) - αⱼ ρ(h c),

so n carries a weight vector of weight μ to one of weight s_α μ = μ - μ(c) α. That is the reflection acting on the weight lattice of the admissible lattice M, realised by an element of the Chevalley group. Since a torus point acts on a weight vector by its character, the conjugate n t(s) n⁻¹ acts on a weight vector of weight μ by (s_α μ)(s), which is the value at μ of the character of the reflected point

s_α(s) = s · α(s)⁻¹ at the coordinate c, and s elsewhere.

Nothing about the ring of points enters: the identities hold over every commutative ring, in particular in characteristics two and three, because the whole content is the rational Lie-algebra identity above transported through the integral divided powers.

The reflection of points is an involution, α(α^∨) = 2 being forced by the sl₂ triple, so the conjugation statement upgrades from an inclusion to the equality of subgroups TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusPoints_range_conj_kostantWeylGL.

Main results

• TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.weylUnit and TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.inv_weylUnit: the Weyl element and its inverse reflect the weight of a weight vector.
• TauCeti.torusCharacter_weylReflectTorusPoint: the reflected point computes the reflected character.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_conj_kostantTorusPoints and TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL_conj_kostantTorusPoints: conjugating a torus point by the Weyl element gives the reflected torus point.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusPoints_range_conj_kostantWeylGL: the Weyl element normalises the split torus.

Roadmap

This completes the normaliser-of-the-torus relation of the pinning data in Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md, and is consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

References

• R. W. Carter, Simple Groups of Lie Type, §§6.4 and 7.2.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• R. Steinberg, Lectures on Chevalley Groups, §3.

theorem TauCeti.UniversalEnvelopingAlgebra.rootWeight_apply_coroot_eq_two {κ : Type u_1} {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {i j : ι} {c : κ} {α : κ → ℤ} (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hαc : ⁅h c, e i⁆ = ↑(α c) • e i) : α c = 2

A root takes the value two at its own coroot. The Cartan index c of the sl₂ triple is the coroot of the weight α of the raising element, so the weight of eᵢ at h c is two.

This is not an extra normalisation: it is forced by the triple relation ⁅h, e⁆ = 2 e, together with e ≠ 0, which the triple also forces since ⁅e, f⁆ = h is nonzero.

The Weyl element reflects weights

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.weylUnit {κ : Type u_1} {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {i j : ι} {c : κ} {α : κ → ℤ} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (j' : κ), ⁅h j', e i⁆ = ↑(α j') • e i) (hαneg : ∀ (j' : κ), ⁅h j', e j⁆ = -(↑(α j') • e j)) {μ : κ → ℤ} {v : V} (hv : IsCartanWeightVector h ρ μ v) : IsCartanWeightVector h ρ (μ - μ c • α) (↑(TauCeti.weylUnit hi hj) v)

The Weyl element reflects weights. A weight vector of weight μ is carried by the Weyl element of the root pair (eᵢ, eⱼ) to a weight vector of the reflected weight s_α μ = μ - μ(c) α, where α is the weight of eᵢ and c is the Cartan index of the coroot.

The proof is the coreflection formula TauCeti.inv_weylUnit_conj_of_lie_eq_smul applied to each designated Cartan operator; no property of μ beyond being a weight is used.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.inv_weylUnit {κ : Type u_1} {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {i j : ι} {c : κ} {α : κ → ℤ} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (j' : κ), ⁅h j', e i⁆ = ↑(α j') • e i) (hαneg : ∀ (j' : κ), ⁅h j', e j⁆ = -(↑(α j') • e j)) {μ : κ → ℤ} {v : V} (hv : IsCartanWeightVector h ρ μ v) : IsCartanWeightVector h ρ (μ - μ c • α) (↑(TauCeti.weylUnit hi hj)⁻¹ v)

The inverse Weyl element reflects weights. The coreflection is an involution on the designated Cartan operators, so conjugating by n⁻¹ reflects a weight exactly as conjugating by n does.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.kostantWeylRestrict {κ : Type u_1} {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {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) {i j : ι} {c : κ} {α : κ → ℤ} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (j' : κ), ⁅h j', e i⁆ = ↑(α j') • e i) (hαneg : ∀ (j' : κ), ⁅h j', e j⁆ = -(↑(α j') • e j)) {μ : κ → ℤ} {v : ↥M} (hv : IsCartanWeightVector h ρ μ ↑v) : IsCartanWeightVector h ρ (μ - μ c • α) ↑((UniversalEnvelopingAlgebra.kostantWeylRestrict e h ρ M hM hi hj) v)

The integral Weyl element of the lattice reflects the weight of a weight vector of the lattice.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.kostantWeylRestrict_symm {κ : Type u_1} {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {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) {i j : ι} {c : κ} {α : κ → ℤ} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (j' : κ), ⁅h j', e i⁆ = ↑(α j') • e i) (hαneg : ∀ (j' : κ), ⁅h j', e j⁆ = -(↑(α j') • e j)) {μ : κ → ℤ} {v : ↥M} (hv : IsCartanWeightVector h ρ μ ↑v) : IsCartanWeightVector h ρ (μ - μ c • α) ↑((UniversalEnvelopingAlgebra.kostantWeylRestrict e h ρ M hM hi hj).symm v)

The inverse of the integral Weyl element reflects the weight of a weight vector of the lattice.

Conjugation of the torus

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_conj_kostantTorusPoints {κ : Type u_1} {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {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) {i j : ι} {c : κ} {α : κ → ℤ} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (j' : κ), ⁅h j', e i⁆ = ↑(α j') • e i) (hαneg : ∀ (j' : κ), ⁅h j', e j⁆ = -(↑(α j') • e j)) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] [DecidableEq κ] {A : Type u_3} [CommRing A] [Algebra ℤ A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (s : κ → Aˣ) : ↑(kostantWeylPoints e h ρ M hM hi hj A) * ↑((kostantTorusPoints M b wt A) s) * ↑(kostantWeylPoints e h ρ M hM hi hj A).symm = ↑((kostantTorusPoints M b wt A) ((weylReflectTorusPoint α c) s))

The Weyl element conjugates a torus point to the reflected torus point. Over every commutative ring of points,

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

with s_α s the reflected point of TauCeti.weylReflectTorusPoint. Both sides are diagonal on the weight basis: n⁻¹ moves a basis vector of weight μ into the space of weight s_α μ, where t(s) scales by (s_α μ)(s), and n moves it back.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL_conj_kostantTorusPoints {κ : Type u_1} {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {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) {i j : ι} {c : κ} {α : κ → ℤ} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (j' : κ), ⁅h j', e i⁆ = ↑(α j') • e i) (hαneg : ∀ (j' : κ), ⁅h j', e j⁆ = -(↑(α j') • e j)) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] [DecidableEq κ] {A : Type u_3} [CommRing A] [Algebra ℤ A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (s : κ → Aˣ) : kostantWeylGL e h ρ M hM hi hj A * (kostantTorusPoints M b wt A) s * (kostantWeylGL e h ρ M hM hi hj A)⁻¹ = (kostantTorusPoints M b wt A) ((weylReflectTorusPoint α c) s)

The Weyl element conjugates a torus point to the reflected torus point, in the general linear group of the points of the lattice.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusPoints_range_conj_kostantWeylGL {κ : Type u_1} {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {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) {i j : ι} {c : κ} {α : κ → ℤ} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (j' : κ), ⁅h j', e i⁆ = ↑(α j') • e i) (hαneg : ∀ (j' : κ), ⁅h j', e j⁆ = -(↑(α j') • e j)) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] {A : Type u_3} [CommRing A] [Algebra ℤ A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (kostantWeylGL e h ρ M hM hi hj A))) (kostantTorusPoints M b wt A).range = (kostantTorusPoints M b wt A).range

The Weyl element normalises the split torus. Conjugation by it permutes the torus points by the reflection s_α, which is an involution, so it carries the group of torus points onto itself.