Documentation

TauCeti.GroupTheory.Coxeter.Length

The parity and the functoriality of the length function of a Coxeter system #

Let cs : CoxeterSystem M W be a Coxeter system. A simple reflection has length one, so it is not the identity and has order exactly two (CoxeterSystem.orderOf_simple).

Left multiplication by a fixed simple reflection changes the length of an element by exactly one (CoxeterSystem.length_mul_mod_two), so it flips the parity of the length. This file packages that pairing as an explicit equivalence CoxeterSystem.lengthParityEquiv between the elements of even length and the elements of odd length, and records its two immediate consequences: the two parity classes are equinumerous, and a Coxeter group with at least one simple reflection has even order. The same fact shows that an element of maximal length in a finite Coxeter group has every simple reflection as a left descent.

Finally, the length function is transported along the two canonical constructions on Coxeter systems, CoxeterSystem.reindex and CoxeterSystem.map: relabelling the simple reflections or pushing the system through a group isomorphism leaves lengths unchanged. Both follow from the fact that a homomorphism carrying simple reflections to simple reflections does not increase length. More generally, length depends only on the indexed simple reflections, even across different Coxeter matrices. These facts feed the Poincaré polynomial in TauCeti/GroupTheory/Coxeter/Poincare.lean.

Main definitions #

Main results #

References #

Simple reflections are involutions #

source
@[simp]
theorem CoxeterSystem.simple_ne_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
cs.simple i ≠ 1

A simple reflection is not the identity: it has length one.

source
@[simp]
theorem CoxeterSystem.orderOf_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
orderOf (cs.simple i) = 2

Each simple reflection has order exactly two.

Left multiplication by a simple reflection flips the parity of the length #

source
theorem CoxeterSystem.length_simple_mul_mod_two {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (w : W) :
cs.length (cs.simple i * w) % 2 = (cs.length w + 1) % 2

Multiplying on the left by a simple reflection changes the length by one, hence changes its residue modulo two.

source
@[simp]
theorem CoxeterSystem.odd_length_simple_mul_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (w : W) :
Odd (cs.length (cs.simple i * w)) ↔ Even (cs.length w)

Left multiplication by a simple reflection turns an element of even length into one of odd length, and only those.

source
@[simp]
theorem CoxeterSystem.even_length_simple_mul_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (w : W) :
Even (cs.length (cs.simple i * w)) ↔ Odd (cs.length w)

Left multiplication by a simple reflection turns an element of odd length into one of even length, and only those.

source
def CoxeterSystem.lengthParityEquiv {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
{ w : W // Even (cs.length w) } ≃ { w : W // Odd (cs.length w) }

Left multiplication by a simple reflection matches the two parity classes. It is an involution of W exchanging the elements of even length with those of odd length.

Instances For
    source
    @[simp]
    theorem CoxeterSystem.lengthParityEquiv_apply_coe {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (x : { w : W // Even (cs.length w) }) :
    ↑((cs.lengthParityEquiv i) x) = cs.simple i * ↑x

    lengthParityEquiv is left multiplication by the simple reflection.

    source
    @[simp]
    theorem CoxeterSystem.lengthParityEquiv_symm_apply_coe {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (x : { w : W // Odd (cs.length w) }) :
    ↑((cs.lengthParityEquiv i).symm x) = cs.simple i * ↑x

    The inverse of lengthParityEquiv is again left multiplication by the simple reflection: the simple reflection is its own inverse.

    source
    theorem CoxeterSystem.natCard_length_even_eq_natCard_length_odd {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Nonempty B] :
    Nat.card { w : W // Even (cs.length w) } = Nat.card { w : W // Odd (cs.length w) }

    The two parity classes of a Coxeter group of positive rank are equinumerous: there are as many elements of even length as of odd length. No finiteness is needed, since the two classes are matched by an explicit bijection.

    source
    theorem CoxeterSystem.even_natCard_of_nonempty_index {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Nonempty B] :
    Even (Nat.card W)

    A Coxeter group of positive rank has even order: a simple reflection is an element of order two, so two divides the order of the group. (For infinite W this reads Even 0, since Nat.card W = 0; the content is the finite case.)

    An element with every simple reflection as a left descent #

    source
    theorem CoxeterSystem.exists_forall_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] :
    ∃ (w : W), ∀ (i : B), cs.IsLeftDescent w i

    A finite Coxeter group has an element of which every simple reflection is a left descent. Any element of maximal length will do: left multiplication by a simple reflection changes the length by one, so it cannot raise it. (There is exactly one such element, the longest element w₀, but uniqueness is not proved here.)

    Transport along a reindexing or a group isomorphism #

    source
    theorem CoxeterSystem.length_apply_le_of_map_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {B' : Type u_3} {H : Type u_4} [Group H] {M' : CoxeterMatrix B'} (cs' : CoxeterSystem M' H) (φ : W →* H) (f : B → B') (hφ : ∀ (i : B), φ (cs.simple i) = cs'.simple (f i)) (w : W) :
    cs'.length (φ w) ≤ cs.length w

    Length does not increase along a homomorphism matching simple reflections: if φ : W →* H carries each simple reflection of cs to a simple reflection of cs', then it carries a word for w to a word of the same length for φ w.

    source
    @[simp]
    theorem CoxeterSystem.wordProd_map {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {H : Type u_4} [Group H] (e : W ≃* H) (ω : List B) :
    (cs.map e).wordProd ω = e (cs.wordProd ω)

    Pushing a word through the isomorphism computes the corresponding word for the transported Coxeter system.

    source
    @[simp]
    theorem CoxeterSystem.length_reindex {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {B' : Type u_3} (e : B ≃ B') (w : W) :
    (cs.reindex e).length w = cs.length w

    The length function is unchanged by reindexing the simple reflections: a bijection of the indexing set carries words to words of the same length.

    source
    @[simp]
    theorem CoxeterSystem.length_map {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {H : Type u_4} [Group H] (e : W ≃* H) (w : W) :
    (cs.map e).length (e w) = cs.length w

    The length function is transported by a group isomorphism: an isomorphism e : W ≃* H matches the simple reflections of cs with those of cs.map e, hence their lengths.

    source
    theorem CoxeterSystem.length_eq_of_simple_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {M' : CoxeterMatrix B} (cs' : CoxeterSystem M' W) (h : ∀ (i : B), cs.simple i = cs'.simple i) (w : W) :
    cs.length w = cs'.length w

    Coxeter systems on the same group with the same indexed simple reflections have the same length function, even if their Coxeter matrices differ.