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

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

Main results

• Ado.isRegularWeight_smul: regularity is invariant under the Weyl group.
• Ado.mem_openDominantChamber_of_isRegularWeight and Ado.isRegularWeight_of_mem_openDominantChamber: the strictly dominant weights are exactly the regular dominant ones.
• Ado.exists_mem_dominantChamber_of_finite_weylGroup and Ado.exists_mem_dominantChamber: every weight is Weyl-conjugate into the closed dominant chamber.
• Ado.iUnion_smul_dominantChamber_eq_univ: the Weyl translates of the closed dominant chamber cover the weight space.
• Ado.ofIdx_smul_notMem_dominantChamber and Ado.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.
• Ado.mem_dominantChamber_iff_forall_mem_posRoots and Ado.mem_openDominantChamber_iff_forall_mem_posRoots: the two chambers are cut out by all of the positive coroot functionals, not just the simple ones.

Implementation notes

The roadmap states this layer over ℝ. Nothing in the argument uses completeness, division, or the archimedean property, so the statements here are made over an arbitrary linearly ordered commutative ring; ℝ and ℚ are the intended instances.

The maximization argument is proved as exists_mem_dominantChamber_of_finite_weylGroup, which asks for no root-system assumption: on top of the standing Finite ι, P.IsCrystallographic and P.IsReduced hypotheses that the positive-root permutation step needs, it assumes only Finite P.weylGroup. The roadmap-signature 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

This file implements the chamber definitions of Layer 4 ("Weyl chambers as cones") and the existence half of its fundamental-domain item (exists_mem_dominantChamber) in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, following the target signatures in that roadmap's Suggested.lean. Uniqueness of the dominant representative is not proved here.

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 Ado.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

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

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

The defining condition of Ado.IsRegularWeight, as an Iff: the predicate is not exposed, so this is how it is introduced and eliminated outside this file.

Not a simp lemma: unfolding the predicate would take Ado.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 Ado.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) : IsRegularWeight P (w • x) ↔ IsRegularWeight P 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 Ado.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) [LinearOrder R] (b : P.Base) : Set M

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

Equations

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

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

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

Equations

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

@[simp]

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

Membership in the closed dominant chamber.

@[simp]

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

Membership in the open dominant chamber.

theorem Ado.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) [LinearOrder R] (b : P.Base) : openDominantChamber P b ⊆ dominantChamber P b

The open dominant chamber is contained in the closed one.

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

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

theorem Ado.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) [LinearOrder R] (b : P.Base) : 0 ∈ dominantChamber P b

The origin is dominant.

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] {x y : M} (hx : x ∈ dominantChamber P b) (hy : y ∈ dominantChamber P b) : x + y ∈ dominantChamber P b

The closed dominant chamber is closed under addition.

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] {t : R} (ht : 0 ≤ t) {x : M} (hx : x ∈ dominantChamber P b) : t • x ∈ dominantChamber P b

The closed dominant chamber is closed under nonnegative scaling.

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

The open dominant chamber is closed under addition.

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

The open dominant chamber is closed under positive scaling.

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] {i : ι} (hi : i ∈ b.support) {x : M} (hx : x ∈ openDominantChamber P b) : RootPairing.weylGroup.ofIdx P i • x ∉ dominantChamber P b

A simple reflection carries every point of the open dominant chamber out of the closed dominant chamber, since it reverses the sign of the corresponding simple coroot.

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] {i : ι} (hi : i ∈ b.support) {x : M} (hx : x ∈ openDominantChamber P b) : RootPairing.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 Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [Finite ↥P.weylGroup] (x : M) : ∃ (w : ↥P.weylGroup), w • x ∈ dominantChamber P 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 Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [Finite ↥P.weylGroup] (x : M) : (MulAction.orbit (↥P.weylGroup) x ∩ dominantChamber P b).Nonempty

Every Weyl orbit meets the closed dominant chamber.

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

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

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem] (x : M) : ∃ (w : ↥P.weylGroup), w • x ∈ dominantChamber P 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 Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} (hx : x ∈ dominantChamber P b) {i : ι} (hi : i ∈ posRoots P b) : 0 ≤ (P.coroot' i) x

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

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} (hx : x ∈ dominantChamber P b) {i : ι} (hi : i ∈ negRoots P b) : (P.coroot' i) x ≤ 0

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

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} (hx : x ∈ openDominantChamber P b) {i : ι} (hi : i ∈ posRoots P b) : 0 < (P.coroot' i) x

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

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} (hx : x ∈ openDominantChamber P b) {i : ι} (hi : i ∈ negRoots P b) : (P.coroot' i) x < 0

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

theorem Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} (hx : x ∈ openDominantChamber P b) : IsRegularWeight P 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 Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} : x ∈ dominantChamber P b ↔ ∀ i ∈ 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 Ado.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) [LinearOrder R] (b : P.Base) [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} : x ∈ openDominantChamber P b ↔ ∀ i ∈ 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.