The dominant chamber of a base

Over a linearly ordered coefficient ring the simple coroots of a base cut the weight space into sign-pattern cones, the Weyl chambers. This file introduces the dominant one, both closed and open, and proves that it meets every Weyl orbit: every weight can be moved into the closed dominant chamber by some element of the Weyl group. Equivalently, the Weyl translates of the closed dominant chamber cover the whole weight space.

The two chambers are defined by the signs of the simple coroot functionals. Since the coroot of a positive root is a nonnegative integer combination of the simple coroots, the same sign conditions in fact hold for all of the positive roots at once, and the file ends by recording that description of both chambers.

The proof is the classical maximization argument. The Weyl group of a finite root system is finite, so the sum of the coroot functionals indexed by the positive roots, evaluated along an orbit, attains a maximum. A simple reflection sᵢ permutes the positive roots other than αᵢ and sends αᵢ to -αᵢ, so applying sᵢ changes that sum by -2⟨αᵢ^∨, x⟩; maximality therefore forces ⟨αᵢ^∨, x⟩ ≥ 0 for every simple root, which is dominance.

The weights lying on none of the walls are the regular ones. Regularity is defined here too, since it is the condition separating the two chambers: a dominant weight is strictly dominant exactly when it is regular. It is stated with no order on the coefficient ring, and is manifestly Weyl-invariant.

Main definitions

• RootPairing.IsRegularWeight is regularity of a weight: no coroot functional vanishes on it.
• RootPairing.dominantChamber is the closed dominant chamber of a base.
• RootPairing.openDominantChamber is its open counterpart.

Main results

• RootPairing.isRegularWeight_smul: regularity is invariant under the Weyl group.
• RootPairing.mem_openDominantChamber_of_isRegularWeight and RootPairing.isRegularWeight_of_mem_openDominantChamber: strict dominance is equivalent to regular dominance.
• RootPairing.exists_mem_dominantChamber_of_finite_weylGroup and RootPairing.exists_mem_dominantChamber: every weight is Weyl-conjugate into the closed dominant chamber.
• RootPairing.iUnion_smul_dominantChamber_eq_univ: the Weyl translates of the closed dominant chamber cover the weight space.
• RootPairing.ofIdx_smul_notMem_dominantChamber and RootPairing.ofIdx_smul_ne_of_mem_openDominantChamber: a simple reflection moves every point of the open dominant chamber, and moves it out of the closed chamber.
• RootPairing.mem_dominantChamber_iff_forall_mem_posRoots and RootPairing.mem_openDominantChamber_iff_forall_mem_posRoots: both chambers are cut out by all of the positive coroot functionals, not just the simple ones.

Implementation notes

The chamber definitions use a preorder on the coefficient ring. Each closure lemma assumes only the monotonicity of addition or multiplication it needs. Reflection sign changes and nonnegative coroot expansions use only ordered addition; strict positivity of the expansions also uses a partial order. The orbit-maximization argument needs a linear order on a characteristic-zero integral domain, but no compatibility of the order with multiplication.

The maximization argument is proved as exists_mem_dominantChamber_of_finite_weylGroup, which does not require the roots to span: it assumes Finite P.weylGroup directly, together with Finite ι, P.IsCrystallographic and P.IsReduced for the positive-root permutation step. The theorem exists_mem_dominantChamber is the root-system case, where that finiteness comes from RootPairing.finite_weylGroup.

Regularity quantifies over all root indices, not just the positive ones. The two are equivalent, since the coroot functional of a negated root is the negative of the original, and quantifying over everything keeps the predicate manifestly Weyl-invariant, which is what the chamber arguments downstream use.

The statements that measure a coroot against the base assume P.flip.IsReduced alongside P.IsReduced; Mathlib's RootPairing.instFlipIsReduced supplies it whenever N is torsion free, which is automatic over a field.

References

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

Regular weights

def RootPairing.IsRegularWeight {ι : 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) (x : M) : Prop

A weight is regular when no coroot functional vanishes on it, that is, when it lies on none of the walls ker αᵢ^∨.

Equations

• P.IsRegularWeight x = ∀ (i : ι), (P.coroot' i) x ≠ 0

theorem RootPairing.isRegularWeight_iff {ι : 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) (x : M) : P.IsRegularWeight x ↔ ∀ (i : ι), (P.coroot' i) x ≠ 0

The defining condition of RootPairing.IsRegularWeight, as an Iff: this introduces and eliminates the predicate without unfolding it outside this file.

Not a simp lemma: unfolding the predicate would take RootPairing.isRegularWeight_smul out of simp-normal form, and would dissolve IsRegularWeight out of the goals its own API is stated about. Use it explicitly, as rw [isRegularWeight_iff] or simp [isRegularWeight_iff].

@[simp]

theorem RootPairing.isRegularWeight_smul {ι : 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) (w : ↥P.weylGroup) (x : M) : P.IsRegularWeight (w • x) ↔ P.IsRegularWeight x

Regularity is a Weyl-invariant condition on weights. A Weyl-group element matches the coroot functional of a root with that of its image, so it can neither create nor destroy a zero.

The dominant chamber

def RootPairing.dominantChamber {ι : 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) (b : P.Base) [Preorder R] : Set M

The closed dominant chamber of a base: the weights on which every simple coroot is nonnegative.

Equations

• P.dominantChamber b = {x : M | ∀ i ∈ b.support, 0 ≤ (P.coroot' i) x}

def RootPairing.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) (b : P.Base) [Preorder R] : Set M

The open dominant chamber of a base: the weights on which every simple coroot is positive.

Equations

• P.openDominantChamber b = {x : M | ∀ i ∈ b.support, 0 < (P.coroot' i) x}

@[simp]

theorem RootPairing.mem_dominantChamber {ι : 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) (b : P.Base) [Preorder R] (x : M) : x ∈ P.dominantChamber b ↔ ∀ i ∈ b.support, 0 ≤ (P.coroot' i) x

Membership in the closed dominant chamber.

@[simp]

theorem RootPairing.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) (b : P.Base) [Preorder R] (x : M) : x ∈ P.openDominantChamber b ↔ ∀ i ∈ b.support, 0 < (P.coroot' i) x

Membership in the open dominant chamber.

theorem RootPairing.openDominantChamber_subset_dominantChamber {ι : 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) (b : P.Base) [Preorder R] : P.openDominantChamber b ⊆ P.dominantChamber b

The open dominant chamber is contained in the closed one.

theorem RootPairing.zero_mem_dominantChamber {ι : 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) (b : P.Base) [Preorder R] : 0 ∈ P.dominantChamber b

The origin is dominant.

theorem RootPairing.add_mem_dominantChamber {ι : 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) (b : P.Base) [Preorder R] [IsOrderedAddMonoid R] {x y : M} (hx : x ∈ P.dominantChamber b) (hy : y ∈ P.dominantChamber b) : x + y ∈ P.dominantChamber b

The closed dominant chamber is closed under addition.

theorem RootPairing.smul_mem_dominantChamber {ι : 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) (b : P.Base) [Preorder R] [PosMulMono R] {t : R} (ht : 0 ≤ t) {x : M} (hx : x ∈ P.dominantChamber b) : t • x ∈ P.dominantChamber b

The closed dominant chamber is closed under nonnegative scaling.

theorem RootPairing.add_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) (b : P.Base) [Preorder R] [AddLeftStrictMono R] {x y : M} (hx : x ∈ P.openDominantChamber b) (hy : y ∈ P.openDominantChamber b) : x + y ∈ P.openDominantChamber b

The open dominant chamber is closed under addition.

theorem RootPairing.smul_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) (b : P.Base) [Preorder R] [PosMulStrictMono R] {t : R} (ht : 0 < t) {x : M} (hx : x ∈ P.openDominantChamber b) : t • x ∈ P.openDominantChamber b

The open dominant chamber is closed under positive scaling.

theorem RootPairing.mem_openDominantChamber_of_isRegularWeight {ι : 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) (b : P.Base) [PartialOrder R] {x : M} (hx : x ∈ P.dominantChamber b) (hreg : P.IsRegularWeight x) : x ∈ P.openDominantChamber b

A dominant weight is strictly dominant as soon as it is regular: nonnegativity that is never an equality is positivity.

theorem RootPairing.ofIdx_smul_notMem_dominantChamber {ι : 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) (b : P.Base) [Preorder R] [IsOrderedAddMonoid R] {i : ι} (hi : i ∈ b.support) {x : M} (hx : 0 < (P.coroot' i) x) : weylGroup.ofIdx P i • x ∉ P.dominantChamber b

A simple reflection carries a weight out of the closed dominant chamber whenever its corresponding simple coroot is positive on that weight.

theorem RootPairing.ofIdx_smul_ne_of_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) (b : P.Base) [Preorder R] [IsOrderedAddMonoid R] {i : ι} (hi : i ∈ b.support) {x : M} (hx : x ∈ P.openDominantChamber b) : weylGroup.ofIdx P i • x ≠ x

No simple reflection fixes a point of the open dominant chamber: it would otherwise stay in the closed dominant chamber.

theorem RootPairing.exists_mem_dominantChamber_of_finite_weylGroup {ι : 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) (b : P.Base) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsOrderedAddMonoid R] [Finite ↥P.weylGroup] (x : M) : ∃ (w : ↥P.weylGroup), w • x ∈ P.dominantChamber b

Every weight is Weyl-conjugate into the closed dominant chamber, for a crystallographic reduced pairing with finitely many roots whose Weyl group is finite. Maximizing posCorootSum along the orbit produces the dominant representative.

theorem RootPairing.orbit_inter_dominantChamber_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) (b : P.Base) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsOrderedAddMonoid R] [Finite ↥P.weylGroup] (x : M) : (MulAction.orbit (↥P.weylGroup) x ∩ P.dominantChamber b).Nonempty

Every Weyl orbit meets the closed dominant chamber.

theorem RootPairing.iUnion_smul_dominantChamber_eq_univ {ι : 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) (b : P.Base) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsOrderedAddMonoid R] [Finite ↥P.weylGroup] : ⋃ (w : ↥P.weylGroup), w • P.dominantChamber b = Set.univ

The Weyl translates of the closed dominant chamber cover the weight space.

theorem RootPairing.exists_mem_dominantChamber {ι : 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) (b : P.Base) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsOrderedAddMonoid R] [P.IsRootSystem] (x : M) : ∃ (w : ↥P.weylGroup), w • x ∈ P.dominantChamber b

Every weight is Weyl-conjugate into the closed dominant chamber. Together with the uniqueness of that representative this says the closed dominant chamber is a fundamental domain for the Weyl group.

theorem RootPairing.coroot'_nonneg_of_mem_posRoots {ι : 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) (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} [Preorder R] [IsOrderedAddMonoid R] (hx : x ∈ P.dominantChamber b) {i : ι} (hi : i ∈ TauCeti.posRoots P b) : 0 ≤ (P.coroot' i) x

Every positive coroot functional is nonnegative on the closed dominant chamber.

theorem RootPairing.coroot'_nonpos_of_mem_negRoots {ι : 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) (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} [Preorder R] [IsOrderedAddMonoid R] (hx : x ∈ P.dominantChamber b) {i : ι} (hi : i ∈ TauCeti.negRoots P b) : (P.coroot' i) x ≤ 0

Every negative coroot functional is nonpositive on the closed dominant chamber.

theorem RootPairing.mem_dominantChamber_iff_forall_mem_posRoots {ι : 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) (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} [Preorder R] [IsOrderedAddMonoid R] : x ∈ P.dominantChamber b ↔ ∀ i ∈ TauCeti.posRoots P b, 0 ≤ (P.coroot' i) x

The closed dominant chamber is cut out by the positive coroot functionals, not just by the simple ones.

theorem RootPairing.coroot'_pos_of_mem_posRoots {ι : 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) (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} [PartialOrder R] [IsOrderedAddMonoid R] (hx : x ∈ P.openDominantChamber b) {i : ι} (hi : i ∈ TauCeti.posRoots P b) : 0 < (P.coroot' i) x

Every positive coroot functional is positive on the open dominant chamber.

theorem RootPairing.coroot'_neg_of_mem_negRoots {ι : 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) (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} [PartialOrder R] [IsOrderedAddMonoid R] (hx : x ∈ P.openDominantChamber b) {i : ι} (hi : i ∈ TauCeti.negRoots P b) : (P.coroot' i) x < 0

Every negative coroot functional is negative on the open dominant chamber.

theorem RootPairing.isRegularWeight_of_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) (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} [PartialOrder R] [IsOrderedAddMonoid R] (hx : x ∈ P.openDominantChamber b) : P.IsRegularWeight x

A strictly dominant weight is regular. Every root is positive or negative, and the two kinds of coroot functional are respectively positive and negative on the open dominant chamber.

theorem RootPairing.mem_openDominantChamber_iff_forall_mem_posRoots {ι : 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) (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} [PartialOrder R] [IsOrderedAddMonoid R] : x ∈ P.openDominantChamber b ↔ ∀ i ∈ TauCeti.posRoots P b, 0 < (P.coroot' i) x

The open dominant chamber is cut out by the positive coroot functionals, not just by the simple ones.