The dot action of the Weyl group on weights #
The dot action of the Weyl group of a base is the linear action conjugated by the translation
by the Weyl vector ρ:
w ⬝ x = w (x + ρ) - ρ.
It is the action that the highest-weight theory runs on, because it is the linear action recentred
at the point -ρ rather than at the origin: -ρ is its fixed point
(TauCeti.dotAction_neg_weylVector), and a simple reflection acts by
sᵢ ⬝ x = x - (⟨x, αᵢ^∨⟩ + 1) αᵢ, so its wall is ⟨x, αᵢ^∨⟩ = -1 instead of ⟨x, αᵢ^∨⟩ = 0.
Everything about it is a transport of the linear theory along the bijection x ↦ x + ρ, and that
is how this file is organized: TauCeti.dotAction_add_weylVector is the equivariance of the shift,
and every later statement is read off from a linear one through it. The one place where the dot
action is genuinely better behaved than the linear action is the closed dominant chamber. The
linear action is free only on the interior of the chamber — a weight on a wall is fixed by the
reflection in that wall — whereas the dot action is free on the whole closed chamber
(TauCeti.eq_one_of_dotAction_eq_self_of_mem_dominantChamber), because the ρ-shift of a dominant
weight is strictly dominant. That freeness is the separation statement the highest-weight theory
needs: distinct dominant weights lie in distinct dot orbits.
Main definitions #
TauCeti.dotAction: the dot actionw ⬝ x = w (x + ρ) - ρof a Weyl-group element on a weight.TauCeti.dotActionPerm: the same, packaged as a group homomorphism intoEquiv.Perm M. The dot action is not registered as aMulActioninstance, since the weight space already carries the linear action of the Weyl group.TauCeti.openDotDominantChamber: the open dominant chamber of the dot action, the weights whoseρ-shift is strictly dominant, equivalently those with-1 < ⟨x, αᵢ^∨⟩for every simple root.
Main results #
TauCeti.dotAction_add_weylVector:w ⬝ x + ρ = w (x + ρ), the equivariance of theρ-shift, from which the action lawsTauCeti.dotAction_oneandTauCeti.dotAction_mulfollow.TauCeti.dotAction_ofIdx: a simple reflection acts bysᵢ ⬝ x = x - (⟨x, αᵢ^∨⟩ + 1) αᵢ, andTauCeti.coroot'_dotAction_ofIdx: it sends the pairing⟨x, αᵢ^∨⟩to-⟨x, αᵢ^∨⟩ - 2.TauCeti.dotAction_ofIdx_eq_self_iff: the wall ofsᵢfor the dot action is⟨x, αᵢ^∨⟩ = -1.TauCeti.eq_one_of_dotAction_eq_self_of_mem_openDotDominantChamber,TauCeti.eq_of_dotAction_eq_of_mem_openDotDominantChamberandTauCeti.dotAction_injective_of_mem_openDotDominantChamber: the dot action is free on its own open dominant chamber, which for a general coefficient ring may be strictly larger than the closed dominant chamber.TauCeti.eq_one_of_dotAction_mem_dominantChamberandTauCeti.eq_one_of_dotAction_eq_self_of_mem_dominantChamber: the dot action is free on the closed dominant chamber, and no nontrivial element keeps a dominant weight dominant.TauCeti.eq_of_dotAction_eq_of_mem_dominantChamberandTauCeti.dotAction_eq_dotAction_iff_of_mem_dominantChamber: a dominant weight is the only dominant weight in its dot orbit, and it is reached by a unique Weyl-group element.
Implementation notes #
The dot action is deliberately not a MulAction instance on M: the weight space already
carries the linear action of P.weylGroup, and a second instance on the same pair of types would
be ambiguous. The action laws are therefore stated as plain lemmas, and
TauCeti.dotActionPerm collects them into a group homomorphism for consumers that want to speak of
orbits or stabilizers.
The definition needs 2 to be invertible in the coefficient ring, since ρ does; nothing else
here asks for more than the statement it appears in. In particular the action laws and the
ρ-shift equivariance are proved with no crystallographic, reduced or order hypothesis, the
simple-reflection formulas add only what TauCeti.reflection_weylVector needs, and the ordered
hypotheses appear only in the dominant-chamber section.
References #
This file supplies the root-pairing-level prerequisite of the dotAction target of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose Layer 7 states "the dot
action w · λ = w(λ+ρ) - ρ is the linear Weyl action recentred at -ρ" and whose
Suggested.lean pins dotAction (base) (w) (lam) on Module.Dual K H; as with
TauCeti.weylVector, the combinatorics lives at the level of an abstract root pairing, so the
Lie-algebra target is a specialization rather than a rebuild. The freeness on the closed dominant
chamber is what the roadmap's centralCharacter_injOn_isDominantIntegral consumes.
The argument is the one in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §13.2 and Ch. VI, §23.3.
The dot action and its action laws #
The dot action of the Weyl group on weights: w ⬝ x = w (x + ρ) - ρ, the linear action
conjugated by the translation by the Weyl vector TauCeti.weylVector.
This is not a MulAction instance: the weight space already carries the linear action of the Weyl
group, and the two would be ambiguous. TauCeti.dotActionPerm packages the action laws as a group
homomorphism.
Equations
- TauCeti.dotAction P b w x = w • (x + TauCeti.weylVector P b) - TauCeti.weylVector P b
Instances For
The dot action is the linear action conjugated by the translation by ρ, by definition.
The ρ-shift is equivariant from the dot action to the linear action: w ⬝ x + ρ is
w (x + ρ). Every statement below is read off from a linear statement through this identity.
The dot action of a Weyl-group element on x, compared with a candidate value y, is the
linear action compared on the ρ-shifts.
The identity acts trivially for the dot action.
The dot action is an action: it turns multiplication in the Weyl group into composition.
Undoing the dot action of w by the dot action of w⁻¹.
Undoing the dot action of w⁻¹ by the dot action of w.
The dot action, as a group homomorphism into the permutations of the weight space. This is
the packaging of TauCeti.dotAction_one and TauCeti.dotAction_mul that lets a consumer speak of
dot orbits and dot stabilizers without a second MulAction instance on the weight space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dot action of a Weyl-group element is injective on weights.
The dot action is faithful. A Weyl-group element fixing every weight for the dot action fixes every weight for the linear action, hence is the identity.
-ρ is the fixed point of the dot action: the dot action is the linear action recentred
there.
A Weyl-group element fixes a weight for the dot action exactly when it fixes its ρ-shift for
the linear action.
Simple reflections #
A simple reflection is an involution for the dot action, as it is for the linear one.
A simple reflection acts by sᵢ ⬝ x = x - (⟨x, αᵢ^∨⟩ + 1) αᵢ for the dot action: the
linear formula with the pairing raised by one.
A simple reflection sends the pairing ⟨x, αᵢ^∨⟩ to -⟨x, αᵢ^∨⟩ - 2 for the dot action.
For sl₂, where α^∨ is the standard coroot, this is the statement that the dot action of the
nontrivial Weyl element sends the weight m to -m - 2.
The wall of sᵢ for the dot action is ⟨x, αᵢ^∨⟩ = -1, not ⟨x, αᵢ^∨⟩ = 0: the dot
action is the linear action recentred at -ρ, and ⟨ρ, αᵢ^∨⟩ = 1.
The open dominant chamber of the dot action #
The open dominant chamber of the dot action: the weights whose ρ-shift is strictly
dominant, equivalently (TauCeti.mem_openDotDominantChamber_iff_neg_one_lt_coroot') those with
-1 < ⟨x, αᵢ^∨⟩ for every simple root αᵢ.
This, and not RootPairing.dominantChamber, is the region the dot action is free on for a general
coefficient ring: the walls of the dot action sit at ⟨x, αᵢ^∨⟩ = -1
(TauCeti.dotAction_ofIdx_eq_self_iff), so this is the open chamber the dot action cuts out. Every
dominant weight lies in it (TauCeti.dominantChamber_subset_openDotDominantChamber), and the
containment may be strict; for integral weights the two conditions agree, since -1 < ⟨x, αᵢ^∨⟩
then forces 0 ≤ ⟨x, αᵢ^∨⟩.
Equations
- TauCeti.openDotDominantChamber P b = {x : M | x + TauCeti.weylVector P b ∈ P.openDominantChamber b}
Instances For
Membership in the open dominant chamber of the dot action, as the strict dominance of the
ρ-shift.
Freeness on the chambers #
The ρ-shift of a weight whose dot translate is dominant is carried into the closed dominant
chamber by the linear action. This is the bridge to the linear freeness statements.
The open dominant chamber of the dot action is cut out by -1 < ⟨x, αᵢ^∨⟩, the walls of
the simple reflections for the dot action (TauCeti.dotAction_ofIdx_eq_self_iff).
A dominant weight lies in the open dominant chamber of the dot action, since the ρ-shift
of a dominant weight is strictly dominant.
The origin lies in the open dominant chamber of the dot action.
Freeness on the open chamber of the dot action #
The dot action is free on its own open dominant chamber: a Weyl-group element fixing a
weight with strictly dominant ρ-shift is the identity.
This is the linear freeness on the open dominant chamber, transported along the ρ-shift; the
freeness on the closed dominant chamber below is its special case, since a dominant weight has a
strictly dominant ρ-shift.
A weight in the open chamber of the dot action is the only such weight in its dot orbit. This is the separation statement the alternating elements of the group algebra consume: distinct weights of the open dot chamber lie in distinct dot orbits.
The dot orbit map of a weight in the open dot chamber is injective: no two Weyl-group elements carry it to the same place.
Freeness on the closed dominant chamber #
A Weyl-group element carrying a dominant weight to a dominant weight for the dot action is
the identity. Unlike the linear action, where a weight on a wall of the chamber is fixed by the
reflection in that wall, the dot action leaves the closed dominant chamber no room: the ρ-shift
of a dominant weight is strictly dominant, and the linear action is free there.
The dot action is free on the closed dominant chamber: a Weyl-group element fixing a dominant weight for the dot action is the identity.
A Weyl-group element carrying a dominant weight to a dominant weight for the dot action fixes it.
A dominant weight is the only dominant weight in its dot orbit. This is the separation statement the highest-weight theory consumes: two dominant weights with the same central character lie in one dot orbit, hence are equal.
The dot action separates dominant weights, and does so with a unique Weyl-group element. Two dot translates of dominant weights agree exactly when the weights agree and the Weyl-group elements agree; in particular distinct dominant weights lie in distinct dot orbits.