The longest element of a finite Weyl group

A finite Weyl group contains exactly one element sending every positive root to a negative root: the longest element w₀. This file constructs it, proves it unique, and records its three defining properties, namely that its inversion set is all of the positive roots, that it maximizes the number of inversions, and that it is an involution.

The construction is the maximization argument. The Weyl group is finite, so some w has as many inversions as possible. If a simple root αᵢ were not an inversion of w, then w sᵢ would have one inversion more, so every simple root is an inversion of w; and a Weyl-group element sending every simple root to a negative root sends every positive root to a negative root, because a positive root is a sum of simple roots and heights add. Uniqueness is the observation that if v and w both reverse all the signs then v⁻¹ w preserves them, so it has no inversions and is the identity.

Since the number of inversions of a Weyl-group element is its Coxeter length, the statements below are the usual ones about w₀: it is the unique element of maximal length, that length is the number of positive roots, and w₀² = 1. The Coxeter presentation of the Weyl group is not available here, so length is spelled throughout as (inversions P b w).ncard.

Main definitions

• TauCeti.longestElement is the longest element w₀ of the Weyl group of a finite root system.

Main results

• TauCeti.exists_inversions_eq_posRoots_of_finite_weylGroup and TauCeti.eq_of_inversions_eq_posRoots: exactly one Weyl-group element inverts every positive root.
• TauCeti.inversions_longestElement and TauCeti.image_weylGroupToPerm_longestElement_posRoots: w₀ exchanges the positive and the negative roots.
• TauCeti.ncard_inversions_le_ncard_inversions_longestElement and TauCeti.eq_longestElement_iff_ncard_inversions: w₀ is the unique element of maximal length, and that length is the number of positive roots.
• TauCeti.isLeast_ncard_posRoots_longestElement: |Φ⁺| simple reflections spell w₀, and no fewer do.
• TauCeti.longestElement_inv and TauCeti.longestElement_sq: w₀ is an involution.
• TauCeti.longestElement_smul_dominantChamber and TauCeti.longestElement_smul_openDominantChamber: w₀ carries the dominant chamber, and its interior, onto its negative, the antidominant chamber.

Implementation notes

TauCeti.longestElement is defined for a root system, where RootPairing.finite_weylGroup supplies the finiteness of the Weyl group. The existence theorem behind it is proved one level more generally, for a crystallographic reduced pairing with finitely many roots whose Weyl group happens to be finite; that is the shape used in TauCeti/LinearAlgebra/RootSystem/Chamber.lean as well.

References

This file implements the "longest element" item of Layer 4 in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. That item spells its length clauses with the Coxeter length of the Weyl Coxeter system, whose construction is the Layer 2 summit and is not yet available. The roadmap pins the two spellings of length to be equal, in its "length equals inversions" item (weylCoxeterSystem P b).length w = (inversions P b w).ncard, so the length statements proved here in the inversion spelling become that item's clauses by rewriting along that identity once it lands. The argument is the one in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §10.3.

theorem TauCeti.mapsTo_negRoots_posRoots_of_inversions_eq_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} [CharZero R] {b : P.Base} {w : ↥P.weylGroup} (h : inversions P b w = posRoots P b) : Set.MapsTo (⇑(P.weylGroupToPerm w)) (negRoots P b) (posRoots P b)

An element inverting every positive root sends every negative root to a positive root, since root negation intertwines the two halves.

theorem TauCeti.inversions_inv_eq_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} [CharZero R] {b : P.Base} {w : ↥P.weylGroup} (h : inversions P b w = posRoots P b) : inversions P b w⁻¹ = posRoots P b

The inverse of an element inverting every positive root inverts every positive root.

theorem TauCeti.mapsTo_posRoots_negRoots_of_forall_mem_support {ι : 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] {w : ↥P.weylGroup} (h : ∀ i ∈ b.support, (P.weylGroupToPerm w) i ∈ negRoots P b) : Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (negRoots P b)

A Weyl-group element sending every simple root to a negative root sends every positive root to a negative root. A positive root is built up from simple roots by addition, and the height of a sum of two roots is the sum of their heights, so the image again has negative height.

theorem TauCeti.inversions_eq_posRoots_of_support_subset {ι : 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] {w : ↥P.weylGroup} (h : ↑b.support ⊆ inversions P b w) : inversions P b w = posRoots P b

A Weyl-group element every simple root of which is an inversion inverts every positive root.

theorem TauCeti.eq_of_inversions_eq_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} [CharZero R] {b : P.Base} [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {v w : ↥P.weylGroup} (hv : inversions P b v = posRoots P b) (hw : inversions P b w = posRoots P b) : v = w

At most one Weyl-group element inverts every positive root. If v and w both do, then v⁻¹ w keeps every positive root positive, hence is the identity.

theorem TauCeti.exists_inversions_eq_posRoots_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) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [Finite ↥P.weylGroup] : ∃ (w : ↥P.weylGroup), inversions P b w = posRoots P b

Some Weyl-group element inverts every positive root, for a crystallographic reduced pairing with finitely many roots whose Weyl group is finite. An element with as many inversions as possible has every simple root among its inversions, since otherwise appending that simple reflection would produce one inversion more.

noncomputable def TauCeti.longestElement {ι : 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] [P.IsRootSystem] : ↥P.weylGroup

The longest element w₀ of a finite Weyl group: the unique element sending every positive root to a negative root. Its inversion set is all of the positive roots, so among all Weyl-group elements it has the most inversions, that is, the greatest Coxeter length.

Equations

• TauCeti.longestElement P b = ⋯.choose

@[simp]

theorem TauCeti.inversions_longestElement {ι : 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] [P.IsRootSystem] : inversions P b (longestElement P b) = posRoots P b

The longest element inverts every positive root.

theorem TauCeti.mapsTo_posRoots_negRoots_longestElement {ι : 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] [P.IsRootSystem] : Set.MapsTo (⇑(P.weylGroupToPerm (longestElement P b))) (posRoots P b) (negRoots P b)

The longest element sends every positive root to a negative root.

theorem TauCeti.mapsTo_negRoots_posRoots_longestElement {ι : 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] [P.IsRootSystem] : Set.MapsTo (⇑(P.weylGroupToPerm (longestElement P b))) (negRoots P b) (posRoots P b)

The longest element sends every negative root to a positive root.

theorem TauCeti.eq_longestElement_of_inversions_eq_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} [CharZero R] {b : P.Base} [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem] {w : ↥P.weylGroup} (h : inversions P b w = posRoots P b) : w = longestElement P b

The longest element is the only Weyl-group element inverting every positive root.

theorem TauCeti.eq_longestElement_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} [CharZero R] {b : P.Base} [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem] {w : ↥P.weylGroup} : w = longestElement P b ↔ inversions P b w = posRoots P b

A Weyl-group element is the longest element exactly when it inverts every positive root.

@[simp]

theorem TauCeti.longestElement_inv {ι : 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] [P.IsRootSystem] : (longestElement P b)⁻¹ = longestElement P b

The longest element is its own inverse. The inverse also inverts every positive root, and only one element does.

@[simp]

theorem TauCeti.longestElement_sq {ι : 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] [P.IsRootSystem] : longestElement P b ^ 2 = 1

The longest element squares to the identity.

theorem TauCeti.smul_smul_longestElement {ι : 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] [P.IsRootSystem] (x : M) : longestElement P b • longestElement P b • x = x

The longest element acts on the weight space as an involution.

theorem TauCeti.weylGroupToPerm_longestElement_involutive {ι : 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] [P.IsRootSystem] : Function.Involutive ⇑(P.weylGroupToPerm (longestElement P b))

The permutation of the root indices induced by the longest element is an involution.

theorem TauCeti.image_weylGroupToPerm_longestElement_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) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem] : ⇑(P.weylGroupToPerm (longestElement P b)) '' posRoots P b = negRoots P b

The longest element exchanges the positive and the negative roots.

theorem TauCeti.image_weylGroupToPerm_longestElement_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) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem] : ⇑(P.weylGroupToPerm (longestElement P b)) '' negRoots P b = posRoots P b

The longest element exchanges the negative and the positive roots.

theorem TauCeti.ncard_inversions_longestElement {ι : 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] [P.IsRootSystem] : (inversions P b (longestElement P b)).ncard = (posRoots P b).ncard

The length of the longest element is the number of positive roots.

theorem TauCeti.isLeast_ncard_posRoots_longestElement {ι : 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] [P.IsRootSystem] : IsLeast {n : ℕ | ∃ (l : List ↥b.support), wordProd P b l = longestElement P b ∧ l.length = n} (posRoots P b).ncard

A shortest word spelling the longest element has one letter for each positive root. This is the acceptance clause ℓ(w₀) = |Φ⁺| in its word-length spelling.

theorem TauCeti.ncard_inversions_le_ncard_inversions_longestElement {ι : 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] [P.IsRootSystem] (w : ↥P.weylGroup) : (inversions P b w).ncard ≤ (inversions P b (longestElement P b)).ncard

No Weyl-group element is longer than the longest element.

theorem TauCeti.eq_longestElement_iff_ncard_inversions {ι : 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] [P.IsRootSystem] {w : ↥P.weylGroup} : w = longestElement P b ↔ (inversions P b w).ncard = (posRoots P b).ncard

The longest element is the unique element of maximal length. An element with as many inversions as there are positive roots has all of them as inversions.

theorem TauCeti.longestElement_ne_one {ι : 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] [P.IsRootSystem] [Nonempty ι] : longestElement P b ≠ 1

A root system with at least one root has a longest element other than the identity.

theorem TauCeti.coroot'_smul_longestElement {ι : 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] [P.IsRootSystem] (i : ι) (x : M) : (P.coroot' i) (longestElement P b • x) = (P.coroot' ((P.weylGroupToPerm (longestElement P b)) i)) x

Evaluating the coroot functional indexed by i on the longest-element translate of a weight x is the same as evaluating the coroot functional indexed by the longest-element image of i on x itself; no inverse appears because the longest element is an involution.

theorem TauCeti.neg_smul_mem_dominantChamber_longestElement {ι : 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] [P.IsRootSystem] {x : M} (hx : x ∈ P.dominantChamber b) : -(longestElement P b • x) ∈ P.dominantChamber b

The longest element carries the dominant chamber into its negative. A simple coroot functional evaluated on w₀ • x is the coroot functional of a negative root evaluated on x, which is nonpositive when x is dominant.

theorem TauCeti.neg_smul_mem_openDominantChamber_longestElement {ι : 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] [P.IsRootSystem] {x : M} (hx : x ∈ P.openDominantChamber b) : -(longestElement P b • x) ∈ P.openDominantChamber b

The longest element carries the interior of the dominant chamber into its negative.

theorem TauCeti.longestElement_smul_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] [P.IsRootSystem] : longestElement P b • P.dominantChamber b = -P.dominantChamber b

The longest element carries the dominant chamber onto its negative, the antidominant chamber. This is the weight-space form of the statement that w₀ reverses the sign of every root.

theorem TauCeti.longestElement_smul_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] [P.IsRootSystem] : longestElement P b • P.openDominantChamber b = -P.openDominantChamber b

The longest element carries the interior of the dominant chamber onto its negative, the interior of the antidominant chamber.