The scaled Weyl elements and their Weyl ratios

Let t : IsSl2Triple H E F be an sl₂ triple in an associative algebra A, with E and F nilpotent, and let A also be an algebra over a commutative ring R. For a unit c of R the rescaled elements c • E and c⁻¹ • F form an sl₂ triple with the same Cartan element (IsSl2Triple.rescale), so the Weyl element of TauCeti/Algebra/Lie/Sl2/Weyl/Automorphism.lean is available at every scale:

n (c) = exp (c • E) · exp (-(c⁻¹ • F)) · exp (c • E),

Chevalley's n_α(c) = x_α(c) x_{-α}(-c⁻¹) x_α(c). Their ratios

h (c) = n (c) · n (1)⁻¹

are the elements denoted h_α(c) = n_α(c) n_α(1)⁻¹ in Chevalley's construction. This file constructs both parameterized families and proves their conjugation relations against the triple. It does not prove that c ↦ h_α(c) is multiplicative, so it does not package this family as a cocharacter.

The scaled Weyl element inverts the Cartan element and interchanges the two nilpotent elements with a scale, n (c) E n (c)⁻¹ = -(c⁻²) • F and n (c) F n (c)⁻¹ = -(c²) • E. If E and F are eigenvectors of ad y with eigenvalues q and -q, respectively, its effect on y is the coreflection y ↦ y - q • H, independently of c. That independence is what makes h (c) centralise every element satisfying those eigenvector hypotheses, while acting on the two root vectors with the expected exponents,

h (c) E h (c)⁻¹ = c² • E,     h (c) F h (c)⁻¹ = c⁻² • F,

Centralisation of a whole Cartan subalgebra is not proved here — this file has no Cartan subalgebra and no root space decomposition. It is the consequence of the displayed hypotheses in a setting supplying them, where every Cartan element y has ⁅y, E⁆ = α(y) • E and ⁅y, F⁆ = -(α(y) • F) for the root α of the triple.

On the root subgroups themselves the same relations read h (c) x_α(u) h (c)⁻¹ = x_α(c² u) and n (c) x_α(u) n (c)⁻¹ = x_{-α}(-c⁻² u), and conjugation carries one scaled Weyl element to another, h (c) n (u) h (c)⁻¹ = n (c² u).

Nothing here needs a Cartan subalgebra, a weight-space decomposition or any finiteness: the whole content is the rescaling of the triple together with the relations already proved for the Weyl element at scale one. The ℚ-algebra hypothesis is inherited from the exponentials, which divide by factorials.

Main definitions

• TauCeti.scaledWeylUnit: the scaled Weyl element n (c).
• TauCeti.weylRatio: the family of Weyl ratios h (c) = n (c) n (1)⁻¹.

Main results

• IsSl2Triple.rescale: rescaling an sl₂ triple by a unit of the base ring.
• TauCeti.scaledWeylUnit_one and TauCeti.weylRatio_one: at scale one the scaled Weyl element is the Weyl element and its ratio is trivial.
• TauCeti.weylRatio_def: the characteristic equation defining the Weyl ratio.
• TauCeti.scaledWeylUnit_eq_weylRatio_mul: the normal form n_α(c) = h_α(c) n_α(1).
• TauCeti.scaledWeylUnit_conj_h, TauCeti.scaledWeylUnit_conj_e, TauCeti.scaledWeylUnit_conj_f: the scaled Weyl element negates the Cartan element and interchanges the two nilpotent elements with images -c⁻² • F and -c² • E.
• TauCeti.scaledWeylUnit_conj_of_lie_eq_smul: the coreflection formula, independent of the scale.
• TauCeti.weylRatio_conj_of_lie_eq_smul and TauCeti.weylRatio_conj_h: the Weyl ratio centralises y whenever E and F are eigenvectors of ad y with opposite eigenvalues.
• TauCeti.weylRatio_conj_e and TauCeti.weylRatio_conj_f: it scales the two nilpotent elements by c² and c⁻².
• TauCeti.weylRatio_conj_exp_smul, TauCeti.weylRatio_conj_exp_neg_smul and TauCeti.scaledWeylUnit_conj_exp_smul: the same relations read on the root subgroup elements.
• The corresponding declarations prefixed by inv_ give the inverse-conjugation rules.
• TauCeti.weylRatio_conj_scaledWeylUnit: conjugation by h (c) carries n (u) to n (c² u).
• TauCeti.lie_weylRatio_conj: the Weyl ratio preserves the eigenspaces of the Cartan element.

References

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

These Weyl-ratio relations are prerequisites for the coroot cocharacter and its relations against the root subgroups, which are part of the pinning data asked for by Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of the CFSGStatement roadmap.

Conjugation by a unit

The scaled Weyl elements

noncomputable def TauCeti.scaledWeylUnit {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (c : Rˣ) : Aˣ

The Weyl element of an sl₂ triple at scale c, the unit exp (c • E) · exp (-(c⁻¹ • F)) · exp (c • E).

For the images of a Chevalley root pair in a representation this is Chevalley's n_α(c) = x_α(c) x_{-α}(-c⁻¹) x_α(c); at c = 1 it is TauCeti.weylUnit.

Equations

• TauCeti.scaledWeylUnit hE hF c = TauCeti.weylUnit ⋯ ⋯

@[simp]

theorem TauCeti.coe_scaledWeylUnit {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (c : Rˣ) : ↑(scaledWeylUnit hE hF c) = IsNilpotent.exp (↑c • E) * IsNilpotent.exp (-(↑c⁻¹ • F)) * IsNilpotent.exp (↑c • E)

The scaled Weyl element is the threefold product of exponentials it is defined to be.

@[simp]

theorem TauCeti.coe_inv_scaledWeylUnit {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (c : Rˣ) : ↑(scaledWeylUnit hE hF c)⁻¹ = IsNilpotent.exp (-(↑c • E)) * IsNilpotent.exp (↑c⁻¹ • F) * IsNilpotent.exp (-(↑c • E))

The inverse of the scaled Weyl element is obtained by negating every exponent.

@[simp]

theorem TauCeti.scaledWeylUnit_one {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) : scaledWeylUnit hE hF 1 = weylUnit hE hF

At scale one the scaled Weyl element is the Weyl element.

The coreflection formula

theorem TauCeti.scaledWeylUnit_conj_of_lie_eq_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) {y : A} {q : ℚ} (hye : ⁅y, E⁆ = q • E) (hyf : ⁅y, F⁆ = -(q • F)) (c : Rˣ) : ↑(scaledWeylUnit hE hF c) * y * ↑(scaledWeylUnit hE hF c)⁻¹ = y - q • H

The coreflection formula does not see the scale. If E and F are eigenvectors of ad y with eigenvalues q and -q, respectively, conjugation by the scaled Weyl element carries y to y - q • H, whatever the scale c.

For a Cartan element y of the triple of a root α this is the coreflection y ↦ y - α(y) • α^∨, and its independence of c is what makes the Weyl ratio TauCeti.weylRatio centralise y (TauCeti.weylRatio_conj_of_lie_eq_smul), hence, in a setting where every Cartan element satisfies these hypotheses, the whole Cartan subalgebra.

theorem TauCeti.scaledWeylUnit_conj_h {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(scaledWeylUnit hE hF c) * H * ↑(scaledWeylUnit hE hF c)⁻¹ = -H

The scaled Weyl element negates the Cartan element of the triple.

theorem TauCeti.scaledWeylUnit_conj_e {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(scaledWeylUnit hE hF c) * E * ↑(scaledWeylUnit hE hF c)⁻¹ = -(↑c⁻¹ ^ 2 • F)

The scaled Weyl element carries the raising element to the lowering element, scaled by c⁻². For a Chevalley root pair this is n_α(c) x_α(u) n_α(c)⁻¹ = x_{-α}(-c⁻² u) read on the Lie-algebra generator.

theorem TauCeti.scaledWeylUnit_conj_f {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(scaledWeylUnit hE hF c) * F * ↑(scaledWeylUnit hE hF c)⁻¹ = -(↑c ^ 2 • E)

The scaled Weyl element carries the lowering element to the raising element, scaled by c².

theorem TauCeti.scaledWeylUnit_conj_exp_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) (u : R) : ↑(scaledWeylUnit hE hF c) * IsNilpotent.exp (u • E) * ↑(scaledWeylUnit hE hF c)⁻¹ = IsNilpotent.exp (-((u * ↑c⁻¹ ^ 2) • F))

Conjugating a root subgroup element by the scaled Weyl element. The exponential of u • E is carried to the exponential of -(c⁻² u) • F; for a Chevalley root pair this is n_α(c) x_α(u) n_α(c)⁻¹ = x_{-α}(-c⁻² u).

theorem TauCeti.scaledWeylUnit_conj_exp_neg_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) (u : R) : ↑(scaledWeylUnit hE hF c) * IsNilpotent.exp (-(u • F)) * ↑(scaledWeylUnit hE hF c)⁻¹ = IsNilpotent.exp ((u * ↑c ^ 2) • E)

Conjugating an opposite root subgroup element by the scaled Weyl element. The exponential of -(u • F) is carried to the exponential of (c² u) • E.

theorem TauCeti.inv_scaledWeylUnit_conj_of_lie_eq_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) {y : A} {q : ℚ} (hye : ⁅y, E⁆ = q • E) (hyf : ⁅y, F⁆ = -(q • F)) (c : Rˣ) : ↑(scaledWeylUnit hE hF c)⁻¹ * y * ↑(scaledWeylUnit hE hF c) = y - q • H

The inverse scaled Weyl element has the same coreflection action as the scaled Weyl element.

theorem TauCeti.inv_scaledWeylUnit_conj_h {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(scaledWeylUnit hE hF c)⁻¹ * H * ↑(scaledWeylUnit hE hF c) = -H

The inverse scaled Weyl element negates the Cartan element.

theorem TauCeti.inv_scaledWeylUnit_conj_e {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(scaledWeylUnit hE hF c)⁻¹ * E * ↑(scaledWeylUnit hE hF c) = -(↑c⁻¹ ^ 2 • F)

The inverse scaled Weyl element carries E to -c⁻² • F.

theorem TauCeti.inv_scaledWeylUnit_conj_f {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(scaledWeylUnit hE hF c)⁻¹ * F * ↑(scaledWeylUnit hE hF c) = -(↑c ^ 2 • E)

The inverse scaled Weyl element carries F to -c² • E.

theorem TauCeti.inv_scaledWeylUnit_conj_exp_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) (u : R) : ↑(scaledWeylUnit hE hF c)⁻¹ * IsNilpotent.exp (u • E) * ↑(scaledWeylUnit hE hF c) = IsNilpotent.exp (-((u * ↑c⁻¹ ^ 2) • F))

Conjugation of a root exponential by the inverse scaled Weyl element.

theorem TauCeti.inv_scaledWeylUnit_conj_exp_neg_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) (u : R) : ↑(scaledWeylUnit hE hF c)⁻¹ * IsNilpotent.exp (-(u • F)) * ↑(scaledWeylUnit hE hF c) = IsNilpotent.exp ((u * ↑c ^ 2) • E)

Conjugation of an opposite-root exponential by the inverse scaled Weyl element.

Weyl ratios

noncomputable def TauCeti.weylRatio {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (c : Rˣ) : Aˣ

The Weyl ratio at c, the element n (c) · n (1)⁻¹ obtained from the scaled Weyl element and the Weyl element.

For the images of a Chevalley root pair in a representation this is Chevalley's h_α(c) = n_α(c) n_α(1)⁻¹. No multiplicativity statement about this parameterized family is made here.

Equations

• TauCeti.weylRatio hE hF c = TauCeti.scaledWeylUnit hE hF c * (TauCeti.weylUnit hE hF)⁻¹

theorem TauCeti.weylRatio_def {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (c : Rˣ) : weylRatio hE hF c = scaledWeylUnit hE hF c * (weylUnit hE hF)⁻¹

The Weyl ratio is the scaled Weyl element multiplied by the inverse scale-one element.

@[simp]

theorem TauCeti.weylRatio_one {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) : weylRatio hE hF 1 = 1

The Weyl ratio at 1 is trivial.

theorem TauCeti.scaledWeylUnit_eq_weylRatio_mul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (c : Rˣ) : scaledWeylUnit hE hF c = weylRatio hE hF c * weylUnit hE hF

The scaled Weyl element factors as its Weyl ratio times the Weyl element: the normal form n_α(c) = h_α(c) n_α(1).

theorem TauCeti.weylRatio_conj_of_lie_eq_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) {y : A} {q : ℚ} (hye : ⁅y, E⁆ = q • E) (hyf : ⁅y, F⁆ = -(q • F)) (c : Rˣ) : ↑(weylRatio hE hF c) * y * ↑(weylRatio hE hF c)⁻¹ = y

The Weyl ratio centralises y when E and F are eigenvectors of ad y with respective eigenvalues q and -q. In the intended application y is an element of a Cartan subalgebra.

theorem TauCeti.weylRatio_conj_e {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(weylRatio hE hF c) * E * ↑(weylRatio hE hF c)⁻¹ = ↑c ^ 2 • E

The Weyl ratio scales the raising element by c².

theorem TauCeti.weylRatio_conj_f {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(weylRatio hE hF c) * F * ↑(weylRatio hE hF c)⁻¹ = ↑c⁻¹ ^ 2 • F

The Weyl ratio scales the lowering element by c⁻².

theorem TauCeti.weylRatio_conj_h {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(weylRatio hE hF c) * H * ↑(weylRatio hE hF c)⁻¹ = H

The Weyl ratio centralises the Cartan element of the triple.

theorem TauCeti.weylRatio_conj_exp_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) (u : R) : ↑(weylRatio hE hF c) * IsNilpotent.exp (u • E) * ↑(weylRatio hE hF c)⁻¹ = IsNilpotent.exp ((u * ↑c ^ 2) • E)

Conjugating a root subgroup element by the Weyl ratio. For a Chevalley root pair this is the relation h_α(c) x_α(u) h_α(c)⁻¹ = x_α(c² u).

theorem TauCeti.weylRatio_conj_exp_neg_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) (u : R) : ↑(weylRatio hE hF c) * IsNilpotent.exp (-(u • F)) * ↑(weylRatio hE hF c)⁻¹ = IsNilpotent.exp (-((u * ↑c⁻¹ ^ 2) • F))

Conjugating the opposite root subgroup element by the Weyl ratio.

theorem TauCeti.inv_weylRatio_conj_of_lie_eq_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) {y : A} {q : ℚ} (hye : ⁅y, E⁆ = q • E) (hyf : ⁅y, F⁆ = -(q • F)) (c : Rˣ) : ↑(weylRatio hE hF c)⁻¹ * y * ↑(weylRatio hE hF c) = y

The inverse Weyl ratio also centralises every element satisfying the opposite-eigenvector hypotheses.

theorem TauCeti.inv_weylRatio_conj_h {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(weylRatio hE hF c)⁻¹ * H * ↑(weylRatio hE hF c) = H

The inverse Weyl ratio centralises the Cartan element.

theorem TauCeti.inv_weylRatio_conj_e {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(weylRatio hE hF c)⁻¹ * E * ↑(weylRatio hE hF c) = ↑c⁻¹ ^ 2 • E

The inverse Weyl ratio scales the raising element by c⁻².

theorem TauCeti.inv_weylRatio_conj_f {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) : ↑(weylRatio hE hF c)⁻¹ * F * ↑(weylRatio hE hF c) = ↑c ^ 2 • F

The inverse Weyl ratio scales the lowering element by c².

theorem TauCeti.inv_weylRatio_conj_exp_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) (u : R) : ↑(weylRatio hE hF c)⁻¹ * IsNilpotent.exp (u • E) * ↑(weylRatio hE hF c) = IsNilpotent.exp ((u * ↑c⁻¹ ^ 2) • E)

Conjugation of a root exponential by the inverse Weyl ratio.

theorem TauCeti.inv_weylRatio_conj_exp_neg_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c : Rˣ) (u : R) : ↑(weylRatio hE hF c)⁻¹ * IsNilpotent.exp (-(u • F)) * ↑(weylRatio hE hF c) = IsNilpotent.exp (-((u * ↑c ^ 2) • F))

Conjugation of an opposite-root exponential by the inverse Weyl ratio.

theorem TauCeti.weylRatio_conj_scaledWeylUnit {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) (c u : Rˣ) : weylRatio hE hF c * scaledWeylUnit hE hF u * (weylRatio hE hF c)⁻¹ = scaledWeylUnit hE hF (c ^ 2 * u)

The Weyl ratio rescales the scaled Weyl elements: conjugation by h_α(c) carries n_α(u) to n_α(c² u).

theorem TauCeti.lie_weylRatio_conj {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {H E F : A} [Algebra ℚ A] (hE : IsNilpotent E) (hF : IsNilpotent F) (ht : IsSl2Triple H E F) {z : A} {m : R} (hhz : ⁅H, z⁆ = m • z) (c : Rˣ) : ⁅H, ↑(weylRatio hE hF c) * z * ↑(weylRatio hE hF c)⁻¹⁆ = m • (↑(weylRatio hE hF c) * z * ↑(weylRatio hE hF c)⁻¹)

The Weyl ratio preserves the eigenspaces of the Cartan element. It centralises H, so conjugation by it commutes with the adjoint action of H.