The Weyl automorphism of an sl₂ triple #
Let t : IsSl2Triple h e f be an sl₂ triple in a Lie algebra L whose raising and lowering
elements act nilpotently. Its Weyl automorphism is the inner automorphism
TauCeti.weylAut t he hf = exp (ad e) ∘ exp (ad (-f)) ∘ exp (ad e),
Chevalley's τ and the Lie-algebra shadow of the group element n_α = x_α(1) x_{-α}(-1) x_α(1)
that represents the reflection s_α in the Weyl group. It negates the whole triple,
h ↦ -h, e ↦ -f, f ↦ -e,
and fixes everything centralised by both e and f. Those two facts are the whole content: the
reflection formula TauCeti.weylAut_apply_of_lie_eq_smul says that an element y acting on e
and f by the opposite scalars c and -c is sent to y - c • h, which on a Cartan subalgebra
is the coreflection in α, and TauCeti.lie_weylAut_apply then transports a simultaneous
eigenvector along it: a z with ⁅y, z⁆ = d • z and ⁅h, z⁆ = m • z has
⁅y, weylAut t he hf z⁆ = (d - c * m) • weylAut t he hf z,
so weylAut t he hf z is again an eigenvector, now for the reflected weight β - β(h) • α.
Everything up to that point is stated for a bare sl₂ triple over a commutative ring K, in terms
of brackets alone: no Cartan subalgebra, no weight-space decomposition and no finiteness. What it
does need is a ℚ-Lie-algebra structure on L, carried as in
TauCeti/Algebra/Lie/InnerAutomorphism.lean by an unbundled [LieAlgebra ℚ L] hypothesis, because
the exponentials divide by factorials; that excludes positive characteristic and non-divisible
bases such as ℤ. The final section specialises to a Lie algebra with non-degenerate Killing form
over a field of characteristic zero, where the eigenvector hypotheses are automatic for elements of
the Cartan subalgebra and the conclusion becomes TauCeti.weylAut_mem_rootSpace and
TauCeti.weylAut_map_rootSpace: the Weyl automorphism of the sl₂ triple of a root α carries the
root space of β onto the root space of β - β(α^∨) • α. Since a nonzero root always admits such a
triple, every reflection in the Weyl group is realised by an automorphism of L
(TauCeti.exists_lieEquiv_forall_mem_rootSpace), which is Humphreys' Proposition 14.3.
This is the step of the Chevalley basis theorem that makes the structure constants of L behave
under the Weyl group: weylAut matches a root vector of β with one of s_α β, and applied to
the triple of α itself it is the source of the relation N (α, β) = -N (-α, -β) between
structure constants (Humphreys §25.2).
A final section takes L to be the commutator algebra of an associative ℚ-algebra A, the case
of a representation. There the Weyl automorphism is inner: TauCeti.weylUnit is the unit
exp E · exp (-F) · exp E of A, Chevalley's group element n_α = x_α(1) x_{-α}(-1) x_α(1), and
TauCeti.weylAut_apply_eq_weylUnit_conj identifies the automorphism with conjugation by it. Every
statement above then reads as a relation in the group of units rather than in the Lie algebra.
Main definitions #
TauCeti.weylAut: the automorphismexp (ad e) ∘ exp (ad (-f)) ∘ exp (ad e)of ansl₂triplet : IsSl2Triple h e f.TauCeti.weylUnit: the unitexp E · exp (-F) · exp Eof an associative algebra containing the triple.
Main results #
TauCeti.weylAut_apply_h,TauCeti.weylAut_apply_e,TauCeti.weylAut_apply_f: the Weyl automorphism negates and swaps the triple.TauCeti.weylAut_apply_of_lie_eq_zero: it fixes the joint centraliser ofeandf.TauCeti.weylAut_apply_of_lie_eq_smul: the reflection formulay ↦ y - c • h.TauCeti.lie_weylAut_apply: the reflected weight of the image of an eigenvector.TauCeti.weylAut_mem_rootSpace,TauCeti.weylAut_map_rootSpaceandTauCeti.exists_lieEquiv_forall_mem_rootSpace: in the Killing setting,weylAutcarries root spaces onto reflected root spaces.TauCeti.weylAut_apply_eq_weylUnit_conj: in an associative algebra the Weyl automorphism is conjugation by the Weyl element.TauCeti.weylUnit_conj_h,TauCeti.weylUnit_conj_e,TauCeti.weylUnit_conj_f,TauCeti.weylUnit_conj_of_lie_eq_smul,TauCeti.inv_weylUnit_conj_of_lie_eq_smulandTauCeti.lie_weylUnit_conj: the conjugation form of the statements above.
References #
The Weyl automorphism exp (ad e) ∘ exp (ad (-f)) ∘ exp (ad e) of an sl₂ triple
t : IsSl2Triple h e f whose raising and lowering elements act nilpotently: the automorphism
realising the reflection in the root of e.
The triple is an argument although the composite itself is a function of e and f alone, so that
the interface asks for the input the name and the results below are about; the reflection is visible
only in the presence of the triple relations, which every result below assumes through t.
Equations
- TauCeti.weylAut _t he hf = (TauCeti.expAd e he).trans ((TauCeti.expAd (-f) ⋯).trans (TauCeti.expAd e he))
Instances For
The Weyl automorphism as the threefold composite it is defined to be. The nilpotency of
ad (-f) is not asked of the caller: it is hf.neg, and any two proofs of it agree.
The two exponentials on the triple #
The values of exp (ad e) and exp (ad (-f)) on h, e and f. Each of these vectors is killed
by at most three brackets, so the truncations of TauCeti/Algebra/Lie/InnerAutomorphism.lean
apply; the two remaining values, exp (ad e) e = e and exp (ad (-f)) f = f, are
TauCeti.expAd_apply_self and TauCeti.expAd_apply_of_lie_eq_zero.
exp (ad e) sends h to h - 2 e.
exp (ad e) sends f to f + h - e.
exp (ad (-f)) sends h to h - 2 f.
exp (ad (-f)) sends e to e + h - f.
The Weyl automorphism on the triple #
The Weyl automorphism negates h.
The Weyl automorphism sends the raising element to minus the lowering element.
The Weyl automorphism sends the lowering element to minus the raising element.
The Weyl automorphism fixes the joint centraliser of e and f.
The reflection formula #
The reflection formula. An element acting on e by a scalar c and on f by -c — for
an sl₂ triple of a root α inside a Cartan subalgebra, an element y with α y = c — is sent
by the Weyl automorphism to y - c • h. This is the coreflection y ↦ y - α y • α^∨.
The Weyl automorphism is an involution on the elements the reflection formula applies to.
The reflected weight. If y acts on e and f by c and -c, and z is a simultaneous
eigenvector of y and h with eigenvalues d and m, then the image of z under the Weyl
automorphism is again an eigenvector of y, with the reflected eigenvalue d - c * m.
The Weyl automorphism reflects root spaces. For the sl₂ triple of a nonzero root α, the
Weyl automorphism carries the root space of a weight β into the root space of the reflection
β - β(α^∨) • α. The nilpotency of ad e and ad f is already forced by the root-space
hypotheses, so it is supplied here rather than asked of the caller.
The Weyl automorphism reflects root spaces, in the sharp form: it carries the root space of
β onto the root space of the reflection β - β(α^∨) • α. The reverse inclusion comes from
TauCeti.weylAut_mem_rootSpace applied to the reflected weight, which the same automorphism sends
back into the root space of β, together with a dimension count.
Every reflection of the root system of (L, H) is realised by an automorphism of L: for a
nonzero root α there is an automorphism carrying the root space of every weight β into the root
space of β - β(α^∨) • α. This is the sl₂ triple of α fed to TauCeti.weylAut, and it needs
no ℚ-structure hypothesis, TauCeti.ratLieAlgebra supplying one.
The Weyl element of a triple in an associative algebra #
When the ambient Lie algebra is the commutator algebra of an associative ℚ-algebra A — the
case of a representation, where A = Module.End ℚ V — the Weyl automorphism is inner: it is
conjugation by the unit
n = exp E · exp (-F) · exp E,
Chevalley's n_α = x_α(1) x_{-α}(-1) x_α(1). This is the passage from the Lie algebra to the
group, and it is what makes the reflection an element of a Chevalley group rather than only an
automorphism of its Lie algebra.
The Weyl element attached to two nilpotent elements in an associative algebra: the unit
exp E · exp (-F) · exp E, whose inverse is exp (-E) · exp F · exp (-E).
For the images of a Chevalley root pair in a representation this is n_α = x_α(1) x_{-α}(-1) x_α(1), the representative of the reflection s_α inside the Chevalley group.
Equations
Instances For
The Weyl element is the threefold product of exponentials it is defined to be.
The inverse of the Weyl element is obtained by negating every exponent.
The Weyl automorphism is conjugation by the Weyl element. Each of the three exponentials
of TauCeti.weylAut acts by conjugation on an associative algebra, so their composite does
too.
The Weyl element negates the Cartan element of the triple.
The Weyl element carries the raising element of the triple to the negated lowering element.
This is the group-level statement that n_α interchanges the root subgroups of α and -α.
The Weyl element carries the lowering element of the triple to the negated raising element.
The reflection formula, at the group level. An element y acting on the raising and
lowering elements by the opposite scalars c and -c — for a Cartan element and the triple of a
root α, an element with α y = c — is carried by conjugation with the Weyl element to
y - c • H, the coreflection y ↦ y - α y • α^∨.
The reflection formula for the inverse Weyl element. The coreflection is an involution on
the elements the reflection formula applies to, so conjugating by n⁻¹ has the same effect as
conjugating by n.
The reflected weight, at the group level. If y acts on the triple by the scalars c and
-c and z is a simultaneous eigenvector of y and H with eigenvalues d and m, then the
conjugate of z by the Weyl element is again an eigenvector of y, with eigenvalue d - c * m.
For a Cartan element y this is the reflection β ↦ β - β(α^∨) • α of weights.