The Weyl representative lies in the elementary group

The Weyl representative of a root pair (eᵢ, eⱼ) is defined in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Weyl.Basic as the scalar extension of an integral automorphism of the admissible lattice, and identified there with the product of divided-power exponentials exp(ρ eᵢ) exp(-ρ eⱼ) exp(ρ eᵢ). This file reads that product in the parametrized root subgroups xᵢ(t) of TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Elementary.Basic:

n = xᵢ(1) xⱼ(-1) xᵢ(1),

so that n is visibly an element of the elementary group generated by the root subgroups.

The two files this sits between are independent of each other, which is why the identification lives here rather than in either. No sl₂ relation between eᵢ and eⱼ is used: the statement is about the three exponentials alone.

Main results

• TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL_eq_kostantRootSubgroupParam_mul: the Weyl representative is the product xᵢ(1) xⱼ(-1) xᵢ(1) of parametrized root-subgroup elements.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL_mem_kostantElementarySubgroup: it therefore belongs to the elementary group.

References

• R. W. Carter, Simple Groups of Lie Type, §6.4.
• R. Steinberg, Lectures on Chevalley Groups, §3.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL_eq_kostantRootSubgroupParam_mul {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) {i j : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (A : CommAlgCat ℤ) : kostantWeylGL e h ρ M hM hi hj ↑A = (kostantRootSubgroupParam e h ρ M hM i hi A) (Multiplicative.ofAdd 1) * (kostantRootSubgroupParam e h ρ M hM j hj A) (Multiplicative.ofAdd (-1)) * (kostantRootSubgroupParam e h ρ M hM i hi A) (Multiplicative.ofAdd 1)

The Weyl representative is the Chevalley product xᵢ(1) xⱼ(-1) xᵢ(1), written in the parametrized root subgroups.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL_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)))) (i j : ι) (A : CommAlgCat ℤ) : kostantWeylGL e h ρ M hM ⋯ ⋯ ↑A ∈ kostantElementarySubgroup e h ρ M hM hnil A

The Weyl representative lies in the elementary group, being a product of three root-subgroup elements.