Inversions of a Weyl-group element that preserves dominance

A Weyl-group element carrying a weight interior to the dominant chamber back into the closed dominant chamber sends no positive root to a negative root, so its inversion set is empty. Since an element with an empty inversion set is the identity, such an element is the identity: the Weyl group acts freely on the interior of the dominant chamber.

Main results

• TauCeti.mapsTo_posRoots_of_smul_mem_dominantChamber: such an element maps positive roots to positive roots.
• TauCeti.inversions_eq_empty_of_smul_mem_dominantChamber and TauCeti.inversions_eq_empty_of_smul_eq_self: its inversion set is empty.
• TauCeti.eq_one_of_smul_mem_dominantChamber: such an element is the identity.
• TauCeti.eq_one_of_smul_eq_self_of_mem_openDominantChamber: the Weyl group acts freely on the interior of the dominant chamber.

References

This file proves the interior case of the uniqueness half of the fundamental-domain item of Layer 4 in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md: for a weight interior to the dominant chamber the moving element is forced to be the identity, and the Weyl group acts freely there. The general case, where a weight on a wall of the chamber is fixed by the reflection in that wall and the moving element need not be the identity, is TauCeti/LinearAlgebra/RootSystem/FundamentalDomain.lean. The proof rests on the chamber definitions in TauCeti/LinearAlgebra/RootSystem/Chamber.lean and the identity criterion for inversion sets in TauCeti/LinearAlgebra/RootSystem/Inversions/StrongExchange.lean. The argument is the one in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §10.

theorem TauCeti.mapsTo_posRoots_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) [LinearOrder R] [IsStrictOrderedRing R] (b : P.Base) [Finite ι] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {x : M} (w : ↥P.weylGroup) (hx : x ∈ P.openDominantChamber b) (hw : w • x ∈ P.dominantChamber b) : Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (posRoots P b)

A Weyl-group element carrying a weight interior to the dominant chamber back into the closed dominant chamber keeps every positive root positive.

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

A Weyl-group element carrying a weight interior to the dominant chamber back into the closed dominant chamber has no inversions.

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

A Weyl-group element fixing a weight interior to the dominant chamber has no inversions.

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

A Weyl-group element carrying a weight interior to the dominant chamber back into the closed dominant chamber is the identity.

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

The Weyl group acts freely on the interior of the dominant chamber.