Length equals inversions #
The number of positive roots that a Weyl-group element sends to negative roots is exactly the
number of letters in a shortest word in the simple reflections spelling that element. One
inequality is the exchange step: a letter changes the inversion count by exactly one, so a word of
k letters cannot spell an element with more than k inversions. The other is a descent
induction: an element other than the identity inverts some simple root, and removing that simple
reflection from the right lowers the inversion count by one, so a word of exactly as many letters
as there are inversions is built up one letter at a time.
The identification is packaged as an IsLeast statement, TauCeti.isLeast_ncard_inversions, so
that both halves are available at once. Everything here is stated and proved purely at the root
level, in terms of TauCeti.inversions and TauCeti.wordProd: no Coxeter presentation is
mentioned, assumed, or needed. Downstream it is the root-level form of the Coxeter length of a
Weyl group, because Mathlib defines CoxeterSystem.length to be exactly the least length of a
word in the simple reflections; so once the Coxeter presentation lands, the Coxeter-length
spelling of this theorem is a rewrite of it rather than a further theorem.
The subadditivity, inversion-invariance and descent consequences recorded here are the standard length-function axioms in their inversion-count spelling.
Main results #
TauCeti.ncard_inversions_wordProd_le_length: a word spells an element with at most as many inversions as the word has letters.TauCeti.exists_wordProd_eq_and_length_eq_ncard_inversions: some word spells the element with exactly as many letters as it has inversions.TauCeti.isLeast_ncard_inversions: the inversion count is the least length of a word spelling the element.TauCeti.ncard_inversions_wordProd_modEq_lengthandTauCeti.length_modEq_length_of_wordProd_eq: every word spelling a given element has the same length parity, namely that of the inversion count.TauCeti.ncard_inversions_invandTauCeti.ncard_inversions_mul_le: the inversion count is invariant under inversion and subadditive.TauCeti.ncard_inversions_mul_ofIdx_lt_of_mem,TauCeti.ncard_inversions_mul_ofIdx_lt_iffandTauCeti.lt_ncard_inversions_mul_ofIdx_iff: right multiplication by the reflection in a positive root lowers the inversion count exactly when that root is an inversion. The reflecting root need not be simple, because the strong exchange condition does not require it to be.TauCeti.ncard_inversions_ofIdx_mul_lt_iffandTauCeti.lt_ncard_inversions_ofIdx_mul_iff: the same criteria for left multiplication, read off the inverse element.
References #
This file iterates over a whole word the root-level exchange step of "Inversion sets and the
exchange step" in Layer 1 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, the item
that asks for exactly that iteration: the step "iterated, is the exchange/deletion condition for
the geometric action and the combinatorial core that Layer 2's generation and presentation
consume". Nothing beyond that Layer 1 material is consumed, and all of it is on main
(TauCeti/LinearAlgebra/RootSystem/Inversions/StrongExchange.lean and its imports).
What Layer 2's presentation takes from the iteration is that a nonempty word of least length
spells an element other than the identity, equivalently that its inversion set is nonempty: that
is how the roadmap proves the lift from the presented group injective in Tits' theorem, "a
nonempty reduced word has a nonempty inversion set". This file therefore precedes
weylCoxeterSystem rather than waiting on it, and the Coxeter-length identity
(weylCoxeterSystem b).length w = (inversions b w).ncard 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, and in Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6.
A word spells an element with at most as many inversions as the word has letters. Each letter changes the inversion count by exactly one, so the count cannot outrun the length.
The inversion count of the element spelled by a word has the parity of the word length. Each letter changes the count by exactly one.
Two words spelling the same Weyl-group element have the same length parity. This is the well-definedness of the sign character of a Weyl group.
Some word spells a Weyl-group element with exactly as many letters as it has inversions.
Length equals inversions. The number of inversions of a Weyl-group element is the least number of simple reflections needed to spell it.
The inversion count is invariant under inversion: reversing a word spelling w spells
w⁻¹, since a simple reflection is its own inverse.
The inversion count is subadditive: concatenating shortest words for v and w spells
v * w.
Right multiplication by the reflection in an inversion shortens. The reflecting root is an arbitrary inversion, not necessarily a simple root, so this is the length inequality for a general reflection of the Weyl group.
Descent criterion. Right multiplication by the reflection in a positive root shortens an element exactly when that root is already an inversion.
Ascent criterion. Right multiplication by the reflection in a positive root lengthens an element exactly when that root is not yet an inversion.
Left descent criterion. Left multiplication by the reflection in a positive root shortens an element exactly when that root is an inversion of the inverse element.
Left ascent criterion. Left multiplication by the reflection in a positive root lengthens an element exactly when that root is not yet an inversion of the inverse element.