The closed dominant chamber is a strict fundamental domain

The Weyl translates of the closed dominant chamber of a base cover the whole weight space (RootPairing.exists_mem_dominantChamber). This file proves that they overlap only where they must: two dominant weights in the same Weyl orbit are equal, and the stabilizer of a dominant weight is generated by the simple reflections in the walls through it. Together with the covering statement this is the closed dominant chamber being a strict fundamental domain for the Weyl group.

For a weight interior to the chamber no wall passes through it, so the stabilizer is trivial and the moving element is the identity; that case is TauCeti.eq_one_of_smul_mem_dominantChamber. The theorems here need no interiority.

The argument is an induction on the number of inversions, run along TauCeti.exists_mem_support_mem_inversions_of_ne_one: a Weyl-group element other than the identity inverts a simple root. If w carries the dominant weight x to a dominant weight and inverts the simple root αᵢ, then ⟨αᵢ^∨, x⟩ is at once nonnegative (x is dominant) and nonpositive (it equals ⟨w αᵢ^∨, w • x⟩, the value of a negative coroot on a dominant weight), so it vanishes: x lies on the wall αᵢ and sᵢ fixes it. Replacing w by w sᵢ moves x to the same place and has one inversion fewer, which is the inductive step.

Main definitions

• TauCeti.wallReflections: the simple reflections of a base whose simple coroot vanishes on a given weight, that is, the reflections in the walls through it. Each of them fixes the weight.

Main results

• TauCeti.mem_closure_wallReflections_of_smul_mem_dominantChamber and TauCeti.stabilizer_eq_closure_wallReflections: the stabilizer of a dominant weight is generated by the simple reflections in the walls through it.
• TauCeti.smul_eq_self_of_smul_mem_dominantChamber and TauCeti.eq_of_mem_orbit_of_mem_dominantChamber: a dominant weight is the only dominant weight in its Weyl orbit.
• TauCeti.existsUnique_mem_orbit_inter_dominantChamber_of_finite_weylGroup and TauCeti.existsUnique_mem_orbit_inter_dominantChamber: every weight has exactly one dominant weight in its Weyl orbit, so the closed dominant chamber is a strict fundamental domain.

Implementation notes

The generation statement is the primitive one here: uniqueness of the dominant representative is read off it, since the generators fix the weight. Stating it needs the walls through a weight as a set of Weyl-group elements, which is TauCeti.wallReflections. That set is cut out by the vanishing of a simple coroot rather than by the fixed-point condition sᵢ • x = x: the vanishing is what the induction produces, and it is the stronger of the two, since sᵢ • x = x says only that ⟨αᵢ^∨, x⟩ • αᵢ vanishes.

Only the existence half needs a finite Weyl group, so it alone carries [Finite P.weylGroup]; the uniqueness statements hold for a crystallographic reduced pairing with finitely many roots and no further hypothesis. As in RootPairing.exists_mem_dominantChamber, the root-system form of the fundamental-domain statement is a corollary of the finite-Weyl-group one.

References

This file completes the fundamental-domain item of Layer 4 in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, whose uniqueness half was previously proved only for weights interior to the chamber. The argument is the one in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §10.3, Theorem (b).

The walls through a weight

def TauCeti.wallReflections {ι : 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) (x : M) : Set ↥P.weylGroup

The reflections in the walls of the dominant chamber of the base b through the weight x: the simple reflections of b whose simple coroot vanishes on x. Each of them fixes x (TauCeti.smul_eq_self_of_mem_wallReflections), but this is cut out by the vanishing rather than by the fixed-point condition, which is weaker in general; see the implementation notes.

Equations

• TauCeti.wallReflections P b x = {w : ↥P.weylGroup | ∃ i ∈ b.support, (P.coroot' i) x = 0 ∧ w = RootPairing.weylGroup.ofIdx P i}

theorem TauCeti.ofIdx_smul_eq_self_of_coroot'_eq_zero {ι : 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} {i : ι} {x : M} (h : (P.coroot' i) x = 0) : RootPairing.weylGroup.ofIdx P i • x = x

A simple reflection whose simple coroot kills a weight fixes that weight.

@[simp]

theorem TauCeti.mem_wallReflections {ι : 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} {x : M} {w : ↥P.weylGroup} : w ∈ wallReflections P b x ↔ ∃ i ∈ b.support, (P.coroot' i) x = 0 ∧ w = RootPairing.weylGroup.ofIdx P i

A Weyl-group element is a wall reflection through x exactly when it is the simple reflection at some simple root whose simple coroot kills x.

theorem TauCeti.ofIdx_mem_wallReflections {ι : 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} {i : ι} {x : M} (hi : i ∈ b.support) (h : (P.coroot' i) x = 0) : RootPairing.weylGroup.ofIdx P i ∈ wallReflections P b x

The reflection in a wall through x belongs to wallReflections.

theorem TauCeti.smul_eq_self_of_mem_wallReflections {ι : 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} {x : M} {w : ↥P.weylGroup} (hw : w ∈ wallReflections P b x) : w • x = x

Every reflection in a wall through x fixes x.

theorem TauCeti.wallReflections_subset_stabilizer {ι : 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} (x : M) : wallReflections P b x ⊆ ↑(MulAction.stabilizer (↥P.weylGroup) x)

The walls through x fix x, so they lie in its stabilizer.

theorem TauCeti.wallReflections_eq_empty_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) [LinearOrder R] {x : M} (hx : x ∈ P.openDominantChamber b) : wallReflections P b x = ∅

No wall of the dominant chamber passes through a weight interior to it.

The stabilizer of a dominant weight

theorem TauCeti.mem_closure_wallReflections_of_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) [LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] (w : ↥P.weylGroup) {x : M} (hx : x ∈ P.dominantChamber b) (hw : w • x ∈ P.dominantChamber b) : w ∈ Subgroup.closure (wallReflections P b x)

A Weyl-group element carrying a dominant weight to a dominant weight is a product of reflections in the walls through that weight.

theorem TauCeti.stabilizer_eq_closure_wallReflections {ι : 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) [LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} (hx : x ∈ P.dominantChamber b) : MulAction.stabilizer (↥P.weylGroup) x = Subgroup.closure (wallReflections P b x)

The stabilizer of a dominant weight is generated by the reflections in the walls through it.

Uniqueness of the dominant representative

theorem TauCeti.smul_eq_self_of_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) [LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] (w : ↥P.weylGroup) {x : M} (hx : x ∈ P.dominantChamber b) (hw : w • x ∈ P.dominantChamber b) : w • x = x

A Weyl-group element carrying a dominant weight to a dominant weight fixes it. No interiority is needed: the element is a product of reflections in walls through the weight, and each of those fixes it.

theorem TauCeti.eq_of_mem_orbit_of_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) [LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x y : M} (hxy : y ∈ MulAction.orbit (↥P.weylGroup) x) (hx : x ∈ P.dominantChamber b) (hy : y ∈ P.dominantChamber b) : y = x

A dominant weight is the only dominant weight in its Weyl orbit.

theorem TauCeti.subsingleton_orbit_inter_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) [LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] (x : M) : (MulAction.orbit (↥P.weylGroup) x ∩ P.dominantChamber b).Subsingleton

A Weyl orbit meets the closed dominant chamber at most once.

theorem TauCeti.existsUnique_mem_orbit_inter_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) [LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] [Finite ↥P.weylGroup] (x : M) : ∃! y : M, y ∈ MulAction.orbit (↥P.weylGroup) x ∩ P.dominantChamber b

The closed dominant chamber is a strict fundamental domain for the Weyl group: every weight has exactly one dominant weight in its Weyl orbit. Only the existence of the representative needs the Weyl group to be finite.

theorem TauCeti.existsUnique_mem_orbit_inter_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) [LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] [P.IsRootSystem] (x : M) : ∃! y : M, y ∈ MulAction.orbit (↥P.weylGroup) x ∩ P.dominantChamber b

The closed dominant chamber of a root system is a strict fundamental domain for the Weyl group: every weight has exactly one dominant weight in its Weyl orbit.