The sign character of a Weyl group #
The Weyl group of a root pairing carries a canonical homomorphism to ℤˣ sending every reflection
to -1. This file builds it as TauCeti.weylSign, from the parity of the inversion count: the
number of positive roots that an element sends to negative roots, taken modulo two.
Two facts make the construction work, and both are already available at the root level. A word in
the simple reflections spells an element whose inversion count has the parity of the word length
(TauCeti.ncard_inversions_wordProd_modEq_length), and every element is spelled by such a word
(TauCeti.exists_wordProd_eq_and_length_eq_ncard_inversions). Concatenating words therefore adds
inversion counts modulo two, which is exactly multiplicativity of (-1) ^ (inversion count). No
Coxeter presentation is used: everything is stated in terms of TauCeti.inversions and
TauCeti.wordProd.
Although the definition names a base, the resulting character does not depend on it. Every root is
Weyl-conjugate to a simple root (TauCeti.exists_mem_support_weylGroupToPerm_eq), and ℤˣ is
commutative, so the reflection in any root — simple or not — has sign -1. Since the reflections
generate the Weyl group, a homomorphism to ℤˣ killing no reflection is unique, and two bases give
the same character.
Main definitions #
TauCeti.weylSign: the sign characterP.weylGroup →* ℤˣof a base,w ↦ (-1) ^ ℓ(w)withℓ(w)the number of inversions.
Main results #
TauCeti.ncard_inversions_mul_modEq: the inversion count is additive modulo two, the fact that makesTauCeti.weylSigna homomorphism.TauCeti.weylSign_ofIdx: every reflection has sign-1, not only the simple ones.TauCeti.weylSign_wordProd: a word ofnletters spells an element of sign(-1) ^ n.TauCeti.weylSign_eq_one_iffandTauCeti.weylSign_eq_neg_one_iff: the sign reads off the parity of the inversion count.TauCeti.eq_weylSign_of_forall_ofIdx: the sign character is the unique homomorphism toℤˣsending every reflection to-1, whenceTauCeti.weylSign_eq_weylSign: it does not depend on the base.TauCeti.weylSign_longestElement: the longest element has sign(-1) ^ |Φ⁺|.
Implementation notes #
The target is ℤˣ rather than a two-element type of one's own, matching Mathlib's
Equiv.Perm.sign and the (-1 : ℤˣ) ^ _ spelling that the Weyl numerator of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md asks for.
TauCeti.weylSign_apply is deliberately not a simp lemma. Unfolding the character back to a
power of -1 would take every lemma below out of simp-normal form, TauCeti.weylSign_ofIdx first
among them; the computations are meant to be done through the named lemmas, not by re-exposing the
inversion count.
The base-independence statement is an equality of homomorphisms rather than a definition of a
base-free weylSign P, because a base is what the inversion count is measured against: there is no
canonical choice to build the definition on, only the theorem that the choice does not matter.
References #
The sign character is the "sgn(w)" of the Weyl numerator
∑_{w ∈ W} sgn(w) e^{w(λ+ρ) - ρ} in Layer 6 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md (the Weyl character formula, the
Weyl dimension formula and Kostant's multiplicity formula are all stated with it), and of the
Tits-sign criterion in the same layer. Its well-definedness is the length-parity statement
TauCeti.length_modEq_length_of_wordProd_eq recorded in Layer 1 of
TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, whose docstring names this character
as its purpose; this file is that prerequisite, built where the inversion combinatorics lives.
The convention follows Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI §1, and J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III §10.3.
The inversion count modulo two #
The inversion count is additive modulo two. Spell each factor by a word of exactly as many letters as it has inversions and concatenate: the product is spelled by a word whose length is the sum of the two lengths, and a word spells an element whose inversion count has the parity of the word length.
Additivity itself fails — TauCeti.ncard_inversions_mul_le is only an inequality — so the parity
is the sharpest statement available, and it is exactly what a sign character needs.
The sign character #
The sign character of a Weyl group, relative to a base: w ↦ (-1) ^ ℓ(w), where ℓ(w) is
the number of positive roots that w sends to negative roots. It is a homomorphism because the
inversion count is additive modulo two, and it does not depend on the base
(TauCeti.weylSign_eq_weylSign).
Equations
- TauCeti.weylSign P b = { toFun := fun (w : ↥P.weylGroup) => (-1) ^ (TauCeti.inversions P b w).ncard, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The sign character is the corresponding power of -1. Not a simp lemma; see the
implementation notes.
Every reflection has sign -1, and not merely the simple ones: a reflection in an
arbitrary root is conjugate to a simple reflection, and ℤˣ is commutative, so conjugation cannot
change the sign.
A word of n letters spells an element of sign (-1) ^ n. In particular all the words
spelling one element have the same length parity, which is the well-definedness that
TauCeti.length_modEq_length_of_wordProd_eq records at the level of inversion counts.
The sign is trivial exactly on the elements with an even number of inversions.
The sign is -1 exactly on the elements with an odd number of inversions.
The sign character is onto ℤˣ as soon as there is a root to reflect in, so the elements
with an even number of inversions form a proper subgroup: the character is not the trivial one,
and the parity it measures is genuine information.
The sign character is intrinsic #
The sign character is the only homomorphism to ℤˣ sending every reflection to -1. The
reflections generate the Weyl group, so a homomorphism out of it is determined by its values on
them; the content is that TauCeti.weylSign takes the prescribed values, which is
TauCeti.weylSign_ofIdx.
The sign character does not depend on the base. Both characters send every reflection to
-1, and that pins a homomorphism to ℤˣ uniquely. So the sign is an invariant of the Weyl group
of the root pairing, even though the inversion count defining it is not.
The parity of the inversion count does not depend on the base either, the pointwise
reading of TauCeti.weylSign_eq_weylSign. The counts themselves need not agree: moving the base
by a Weyl-group element conjugates the element whose inversions are being counted, and conjugate
elements have different lengths in general.
The longest element #
The longest element has sign (-1) ^ |Φ⁺|: it inverts every positive root, so its
inversion count is the number of positive roots.