The Weyl vector of a base

The Weyl vector ρ of a base of a root pairing is the half-sum of the positive roots. It is the shift that turns the Weyl group action on weights into the dot action, and it appears in the Weyl character, dimension and Kostant formulas as the correction λ ↦ λ + ρ.

Which roots are positive is defined only over a coefficient ring of characteristic zero, and halving asks for 2 to be invertible on top of that. So the sum of the positive roots is introduced first, as TauCeti.twoWeylVector, over a characteristic-zero coefficient ring, and the Weyl vector itself only once 2 is invertible as well. The simple-coroot pairing and the simple reflection identity are proved for the sum first and then divided by two; the statements that speak of ρ alone — the dot action and the dominance results — are proved only in the halved form. So nothing below assumes more of the coefficient ring than its own statement needs.

The one theorem the notion exists for is that ρ pairs to 1 with every simple coroot, equivalently that the simple reflection sᵢ sends ρ to ρ - αᵢ. Its proof is the classical one: sᵢ negates αᵢ and permutes the remaining positive roots, so the pairings of those remaining roots with αᵢ^∨ cancel in pairs and only ⟨αᵢ, αᵢ^∨⟩ = 2 survives.

Main definitions

• TauCeti.twoWeylVector: the sum of the positive roots, that is 2ρ.
• TauCeti.weylVector: the Weyl vector ρ, the half-sum of the positive roots, defined when 2 is invertible in the coefficient ring.

Main results

• TauCeti.coroot'_twoWeylVector and TauCeti.coroot'_weylVector: ⟨2ρ, αᵢ^∨⟩ = 2 and ⟨ρ, αᵢ^∨⟩ = 1 for every simple root αᵢ.
• TauCeti.reflection_twoWeylVector and TauCeti.reflection_weylVector: sᵢ(2ρ) = 2ρ - 2αᵢ and sᵢ(ρ) = ρ - αᵢ.
• TauCeti.sum_root_negRootsFinset: the sum of the negative roots is -2ρ.
• TauCeti.reflection_add_weylVector_sub_weylVector: the dot action of a simple reflection, sᵢ ⬝ λ = λ - (⟨λ, αᵢ^∨⟩ + 1) αᵢ.
• TauCeti.add_weylVector_mem_openDominantChamber and TauCeti.weylVector_mem_openDominantChamber: over a linearly ordered coefficient ring the ρ-shift of a dominant weight is strictly dominant, and ρ itself is a regular weight.
• TauCeti.openDominantChamber_nonempty: consequently the open dominant chamber has a point, which over a general coefficient ring is a genuine hypothesis rather than a formality.

References

This file supplies the root-pairing-level prerequisite of the ρ item of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: Layer 1 there "only fixes the notation ρ for the half-sum of positive roots and states dominance and integrality of weights", and the Lie-algebra signature weylVector (base : (LieAlgebra.IsKilling.rootSystem H).Base) : Module.Dual K H is stated in the Layer 5 section of that roadmap's Suggested.lean, where the Casimir eigenvalue is the first consumer; the Weyl character and dimension formulas of Layer 6 are stated in terms of the same ρ. Nothing here is a Lie-algebra-level declaration, and nothing here uses the highest-weight machinery of Layers 2-4: ρ is built for an abstract root pairing, where the positive-root combinatorics it needs already lives, so that the Lie-algebra target is a specialization rather than a rebuild.

The argument is the one in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §10.2 and §13.3.

noncomputable def TauCeti.twoWeylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : M

Twice the Weyl vector: the sum of the positive roots of a base.

The Weyl vector itself is TauCeti.weylVector, this element halved; it needs 2 to be invertible in the coefficient ring, whereas the sum needs only the characteristic-zero hypothesis under which the positive roots are defined at all, and carries all the content.

Equations

• TauCeti.twoWeylVector P b = ∑ i ∈ TauCeti.posRootsFinset P b, P.root i

theorem TauCeti.twoWeylVector_def {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : twoWeylVector P b = ∑ i ∈ posRootsFinset P b, P.root i

2ρ is the sum of the positive roots, by definition.

theorem TauCeti.coroot'_twoWeylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : (P.coroot' i) (twoWeylVector P b) = 2

The sum of the positive roots pairs to 2 with every simple coroot. All the positive roots other than αᵢ cancel, leaving ⟨αᵢ, αᵢ^∨⟩ = 2.

Not @[simp]: RootPairing.coroot' is an abbrev, so simp unfolds this left-hand side through LinearMap.flip_apply and the simpNF linter rejects the tag. The simp-usable form of this identity is TauCeti.reflection_twoWeylVector below.

@[simp]

theorem TauCeti.reflection_twoWeylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : (P.reflection i) (twoWeylVector P b) = twoWeylVector P b - 2 • P.root i

A simple reflection subtracts 2αᵢ from the sum of the positive roots.

theorem TauCeti.sum_root_negRootsFinset {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : ∑ i ∈ negRootsFinset P b, P.root i = -twoWeylVector P b

The sum of the negative roots is -2ρ. Root negation is a bijection from the negative roots onto the positive ones.

noncomputable def TauCeti.weylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [Invertible 2] : M

The Weyl vector ρ: the half-sum of the positive roots of a base.

Equations

• TauCeti.weylVector P b = ⅟2 • TauCeti.twoWeylVector P b

theorem TauCeti.weylVector_def {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [Invertible 2] : weylVector P b = ⅟2 • twoWeylVector P b

ρ is half the sum of the positive roots, by definition.

@[simp]

theorem TauCeti.two_smul_weylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [Invertible 2] : 2 • weylVector P b = twoWeylVector P b

Doubling the Weyl vector recovers the sum of the positive roots.

theorem TauCeti.coroot'_weylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [Invertible 2] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : (P.coroot' i) (weylVector P b) = 1

The Weyl vector pairs to 1 with every simple coroot, ⟨ρ, αᵢ^∨⟩ = 1. This is the characteristic pairing identity that ρ is introduced for; it records the values of ρ on the simple coroots, and over an abstract root pairing those values need not pin ρ down, since nothing here says the simple coroots separate the points of M.

Not @[simp], for the same reason as TauCeti.coroot'_twoWeylVector.

@[simp]

theorem TauCeti.reflection_weylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [Invertible 2] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : (P.reflection i) (weylVector P b) = weylVector P b - P.root i

A simple reflection subtracts its simple root from the Weyl vector, sᵢ(ρ) = ρ - αᵢ.

theorem TauCeti.coroot'_add_weylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [Invertible 2] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) (x : M) : (P.coroot' i) (x + weylVector P b) = (P.coroot' i) x + 1

The ρ-shift raises every simple coroot pairing by one. This is the whole role of ρ in the highest-weight theory: it converts the dominance condition 0 ≤ ⟨λ, αᵢ^∨⟩ into the strict one 0 < ⟨λ + ρ, αᵢ^∨⟩.

theorem TauCeti.reflection_add_weylVector_sub_weylVector {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [Invertible 2] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) (x : M) : (P.reflection i) (x + weylVector P b) - weylVector P b = x - ((P.coroot' i) x + 1) • P.root i

The dot action of a simple reflection. Conjugating the reflection sᵢ by the translation by ρ gives sᵢ ⬝ λ = λ - (⟨λ, αᵢ^∨⟩ + 1) αᵢ. Only this formula on weights is proved here; it is the shifted Weyl group action that the highest-weight theory uses in place of the linear one, but the statement that it permutes the highest weights of a given central character belongs to that setting and needs its hypotheses.

theorem TauCeti.add_weylVector_mem_openDominantChamber {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [LinearOrder R] [IsStrictOrderedRing R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {x : M} (hx : x ∈ dominantChamber P b) : x + weylVector P b ∈ openDominantChamber P b

Shifting a dominant weight by ρ makes it strictly dominant.

theorem TauCeti.weylVector_mem_openDominantChamber {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [LinearOrder R] [IsStrictOrderedRing R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] : weylVector P b ∈ openDominantChamber P b

The Weyl vector is strictly dominant, hence a regular weight: it lies on no wall of the dominant chamber.

theorem TauCeti.openDominantChamber_nonempty {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [LinearOrder R] [IsStrictOrderedRing R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] : (openDominantChamber P b).Nonempty

The open dominant chamber is nonempty once 2 is invertible: the Weyl vector ρ pairs to 1 with every simple coroot, so it is strictly dominant.