Basic properties of the Weyl element of a Kostant root subgroup pair

Let U_ℤ = kostantForm e h act on a rational vector space V through ρ, let M ≤ V be a U_ℤ-stable additive subgroup, and let eᵢ, eⱼ be distinguished root vectors whose images span, together with a distinguished Cartan vector h c, an sl₂ triple in Module.End ℚ V. Chevalley's Weyl element is the product of root subgroup elements

n = x_i(1) x_j(-1) x_i(1),

the group-level representative of the reflection s_α for α the root of eᵢ.

Its two defining properties are proved here over an arbitrary commutative ring of points, not only over ℚ. First, n is defined over ℤ: the three exponentials have integer parameters, so TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints is the scalar extension of one integral automorphism of the lattice M, namely the restriction of the unit TauCeti.weylUnit = exp ρ(eᵢ) · exp (-ρ(eⱼ)) · exp ρ(eᵢ) of Module.End ℚ V. Second, conjugation by it interchanges the two root subgroups with a sign,

n x_i(u) n⁻¹ = x_j(-u)     for every u in the ring of points,

which is TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_conj_baseChangeExp. Nothing about the parameter ring enters that proof: the whole content is the Lie-algebra identity n ρ(eᵢ) n⁻¹ = -ρ(eⱼ) of TauCeti.weylUnit_conj_e, which passes through the divided powers because conjugation by a unit is an algebra automorphism. In particular the relation holds in characteristic two and three, where the exponential series itself is unavailable.

The same mechanism gives the action on weights: TauCeti.UniversalEnvelopingAlgebra.weylUnit_apply_eigenvector says that n carries an eigenvector of ρ(h c) of eigenvalue m to an eigenvector of eigenvalue -m. When the original vector lies in M, TauCeti.UniversalEnvelopingAlgebra.weylUnit_smul_mem separately shows that its image again lies in M. That is the reflection s_α acting on the weight lattice, realised by an element of the Chevalley group rather than only by an automorphism of the Lie algebra.

This is the normaliser-of-the-torus half of the pinning data of Layer 9 of the ReductiveGroups roadmap: the Chevalley commutator relations in TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/Commutator/Basic.lean and TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/Commutator/G2/Basic.lean describe how two root subgroups interact, and the relations here describe how the reflection permutes them.

Main definitions

• TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints: the Weyl element on points valued in an arbitrary commutative ring.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL: the same element of the general linear group of those points.

Main results

• TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_toLinearMap_eq: it is the product x_i(1) x_j(-1) x_i(1) of root subgroup elements.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_conj_baseChangeExp: conjugating the root subgroup of eᵢ by it gives the root subgroup of eⱼ with a negated parameter.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantWeylPoints: it is natural in the ring of points.
• TauCeti.UniversalEnvelopingAlgebra.weylUnit_apply_eigenvector: it reflects the weight of an eigenvector of a distinguished Cartan vector.

References

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

Stability of the lattice under the Weyl element

theorem TauCeti.UniversalEnvelopingAlgebra.weylUnit_smul_mem {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {v : V} (hv : v ∈ M) : ↑(weylUnit hi hj) • v ∈ M

The Weyl element of a Kostant root pair preserves the lattice: it is a product of root subgroup elements at integer parameters, each of which does.

theorem TauCeti.UniversalEnvelopingAlgebra.inv_weylUnit_smul_mem {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {v : V} (hv : v ∈ M) : ↑(weylUnit hi hj)⁻¹ • v ∈ M

The inverse of the Weyl element preserves the lattice, by the same computation with every exponent negated.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeylRestrict {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) : ↥M ≃ₗ[ℤ] ↥M

The Weyl element restricted to an integral automorphism of the lattice.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantWeylRestrict e h ρ M hM hi hj = TauCeti.integralUnitRestrict (TauCeti.weylUnit hi hj) M ⋯ ⋯

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantWeylRestrict_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (v : ↥M) : ↑((kostantWeylRestrict e h ρ M hM hi hj) v) = ↑(weylUnit hi hj) • ↑v

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantWeylRestrict_symm_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (v : ↥M) : ↑((kostantWeylRestrict e h ρ M hM hi hj).symm v) = ↑(weylUnit hi hj)⁻¹ • ↑v

The inverse of the restricted Weyl element acts by the inverse of the Weyl element.

The Weyl element on points

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (A : Type u_3) [CommRing A] [Algebra ℤ A] : TensorProduct ℤ A ↥M ≃ₗ[A] TensorProduct ℤ A ↥M

The Weyl element of a Kostant root pair, on points valued in a commutative ring A.

It is the scalar extension of a single integral automorphism of the lattice M. That it is also the Chevalley product x_i(1) x_j(-1) x_i(1) of root subgroup elements is TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_toLinearMap_eq.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints e h ρ M hM hi hj A = LinearEquiv.baseChange ℤ A (↥M) (↥M) (TauCeti.UniversalEnvelopingAlgebra.kostantWeylRestrict e h ρ M hM hi hj)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_toLinearMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] : ↑(kostantWeylPoints e h ρ M hM hi hj A) = LinearMap.baseChange A ↑(kostantWeylRestrict e h ρ M hM hi hj)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_symm_toLinearMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] : ↑(kostantWeylPoints e h ρ M hM hi hj A).symm = LinearMap.baseChange A ↑(kostantWeylRestrict e h ρ M hM hi hj).symm

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_apply_tmul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] (r : A) (v : ↥M) : (kostantWeylPoints e h ρ M hM hi hj A) (r ⊗ₜ[ℤ] v) = r ⊗ₜ[ℤ] (kostantWeylRestrict e h ρ M hM hi hj) v

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_symm_apply_tmul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] (r : A) (v : ↥M) : (kostantWeylPoints e h ρ M hM hi hj A).symm (r ⊗ₜ[ℤ] v) = r ⊗ₜ[ℤ] (kostantWeylRestrict e h ρ M hM hi hj).symm v

The inverse Weyl element on points acts on a pure tensor through the inverse of the integral automorphism.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (A : Type u_3) [CommRing A] [Algebra ℤ A] : LinearMap.GeneralLinearGroup A (TensorProduct ℤ A ↥M)

The Weyl element of a Kostant root pair as an element of the general linear group of the points of the lattice.

This is the automorphism TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints, packaged so that it multiplies with the root subgroups and the split torus, which are group-valued.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL e h ρ M hM hi hj A = LinearMap.GeneralLinearGroup.ofLinearEquiv (TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints e h ρ M hM hi hj A)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL_val {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] : ↑(kostantWeylGL e h ρ M hM hi hj A) = ↑(kostantWeylPoints e h ρ M hM hi hj A)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL_inv_val {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] : ↑(kostantWeylGL e h ρ M hM hi hj A)⁻¹ = ↑(kostantWeylPoints e h ρ M hM hi hj A).symm

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_toLinearMap_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] : ↑(kostantWeylPoints e h ρ M hM hi hj A) = baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M ⋯ 1 * baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j))) M ⋯ (-1) * baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M ⋯ 1

The Weyl element is the Chevalley product x_i(1) x_j(-1) x_i(1).

Each factor is a root subgroup element at an integer parameter, hence already defined over ℤ; this identifies their product with the scalar extension of the integral automorphism TauCeti.UniversalEnvelopingAlgebra.kostantWeylRestrict.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylPoints_conj_baseChangeExp {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] (u : A) : ↑(kostantWeylPoints e h ρ M hM hi hj A) * baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M ⋯ u * ↑(kostantWeylPoints e h ρ M hM hi hj A).symm = baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j))) M ⋯ (-u)

Conjugation by the Weyl element interchanges the two root subgroups. Over every ring of points, n x_i(u) n⁻¹ = x_j(-u).

Only the Lie-algebra relation n ρ(eᵢ) n⁻¹ = -ρ(eⱼ) is used, so the identity is insensitive to the characteristic of the ring of points.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantWeylPoints_algHom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] {B : Type u_3} [CommRing B] [Algebra ℤ B] (φ : A →ₐ[ℤ] B) (z : TensorProduct ℤ A ↥M) : (TensorProduct.map φ.toLinearMap LinearMap.id) ((kostantWeylPoints e h ρ M hM hi hj A) z) = (kostantWeylPoints e h ρ M hM hi hj B) ((TensorProduct.map φ.toLinearMap LinearMap.id) z)

The Weyl element is natural in the ring of points: it is the scalar extension of a single integral automorphism, so applying a ring homomorphism to the scalar coordinate of every tensor intertwines the two.

This is the form for parameter rings carrying explicit ℤ-algebra structures; the version for an arbitrary ring homomorphism is TauCeti.UniversalEnvelopingAlgebra.map_kostantWeylPoints.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantWeylPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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 : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] (φ : A →+* B) (z : TensorProduct ℤ A ↥M) : (TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) ((kostantWeylPoints e h ρ M hM hi hj A) z) = (kostantWeylPoints e h ρ M hM hi hj B) ((TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) z)

The Weyl element is natural in the ring of points, for every homomorphism of commutative rings of points: a ℤ-algebra structure on a ring is unique, so no compatibility with a chosen one is needed.

The reflected weight

theorem TauCeti.UniversalEnvelopingAlgebra.weylUnit_apply_eigenvector {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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)))) {v : V} {m : ℚ} (hmv : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) v = m • v) : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (↑(weylUnit hi hj) v) = -m • ↑(weylUnit hi hj) v

The Weyl element reflects weights. If v is an eigenvector of a distinguished Cartan vector with eigenvalue m, then its image under the Weyl element is an eigenvector with the reflected eigenvalue -m. If additionally v ∈ M, then TauCeti.UniversalEnvelopingAlgebra.weylUnit_smul_mem separately shows that the image lies in the lattice.

For the sl₂ triple of a root α this is the reflection s_α acting on the weight lattice of M, realised by an element of the Chevalley group rather than only by an automorphism of the Lie algebra.