The Poincaré polynomial of a finite Coxeter system

For a Coxeter system cs : CoxeterSystem M W with W finite, the length generating function ∑_{w ∈ W} q^{ℓ(w)} is a genuine polynomial with integer coefficients, the Poincaré polynomial of cs. This file introduces it and proves the elementary facts that make it a generating function: its coefficient at k counts the elements of length k, its value at 1 is the order of W, its constant term is 1, and its degree is the largest length occurring in W.

The theorem with content beyond bookkeeping is the value at -1. Left multiplication by a fixed simple reflection is a sign-reversing involution of W (CoxeterSystem.length_simple_mul_mod_two), so the alternating sum ∑_{w ∈ W} (-1)^{ℓ(w)} vanishes as soon as there is at least one simple reflection. The parity bookkeeping itself, together with the equivalence between the two parity classes, lives in TauCeti/GroupTheory/Coxeter/Length.lean.

At the other extreme, a Coxeter system indexed by an empty type has a trivial group -- every element is the product of a word in the generators, and there are no generators -- so its Poincaré polynomial is 1. That degenerate case is recorded as well, since it is what pins the normalisation of the constant term.

Main definitions

• TauCeti.poincarePolynomial: the Poincaré polynomial ∑_{w ∈ W} q^{ℓ(w)} ∈ ℤ[q] of a Coxeter system on a finite group.

Main results

• TauCeti.coeff_poincarePolynomial: the coefficient of q^k counts the elements of length k.
• TauCeti.eval_one_poincarePolynomial: the value at 1 is |W|.
• TauCeti.eval_neg_one_poincarePolynomial: the value at -1 is 0 when the simple reflections are indexed by a nonempty type.
• TauCeti.natDegree_poincarePolynomial and TauCeti.leadingCoeff_poincarePolynomial: the degree is the maximal length, and the leading coefficient counts the elements attaining it.
• TauCeti.poincarePolynomial_reindex and TauCeti.poincarePolynomial_map: the polynomial is invariant under the two canonical transports of a Coxeter system.
• TauCeti.poincarePolynomial_of_isEmpty and TauCeti.poincarePolynomial_of_unique_index: the two smallest cases, 1 in rank 0 and 1 + q in rank 1.

Implementation notes

The polynomial is defined and its intrinsic properties are stated under [Finite W], the enumeration being supplied internally by Fintype.ofFinite; only the lemmas whose right-hand side is itself a Finset.univ expression (the two unfolding lemmas) ask for [Fintype W]. Counts are stated with Nat.card on a subtype rather than with a Finset.filter, so that no DecidableEq or DecidablePred argument leaks into the statements, and the degree is characterised by IsGreatest on the range of the length function rather than by a Finset.sup.

coeff_poincarePolynomial carries @[simp low] rather than a plain @[simp]: the specialised coeff_poincarePolynomial_zero must fire first, since at equal priority the general lemma rewrites its left-hand side and the simpNF linter then reports the constant-term lemma as not being in simp-normal form.

Nothing here needs the group to be finitely generated, crystallographic, or attached to a root system: the statements are about an arbitrary Coxeter system, which is where the roadmap places them.

References

This is the "length generating function ... the Poincaré polynomial" item among the consequences of Layer 3 ("the missing Coxeter combinatorics") in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md.

• A. Björner and F. Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), Sections 1.4 and 7.1.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Section 1.11.

noncomputable def TauCeti.poincarePolynomial {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] : Polynomial ℤ

The Poincaré polynomial of a Coxeter system on a finite group: the length generating function ∑_{w ∈ W} q^{ℓ(w)}, viewed as an element of ℤ[q].

theorem TauCeti.poincarePolynomial_eq_sum {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Fintype W] : poincarePolynomial cs = ∑ w : W, Polynomial.X ^ cs.length w

The Poincaré polynomial, unfolded.

theorem TauCeti.eval_poincarePolynomial {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Fintype W] (q : ℤ) : Polynomial.eval q (poincarePolynomial cs) = ∑ w : W, q ^ cs.length w

Evaluating the Poincaré polynomial at q gives the length generating function ∑ q^{ℓ(w)}.

@[simp]

theorem TauCeti.coeff_poincarePolynomial {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] (k : ℕ) : (poincarePolynomial cs).coeff k = ↑(Nat.card { w : W // cs.length w = k })

The Poincaré polynomial is the length generating function: its coefficient at q^k is the number of elements of W of length k.

theorem TauCeti.coeff_poincarePolynomial_nonneg {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] (k : ℕ) : 0 ≤ (poincarePolynomial cs).coeff k

The coefficients of the Poincaré polynomial are nonnegative, being cardinalities.

@[simp]

theorem TauCeti.coeff_poincarePolynomial_zero {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] : (poincarePolynomial cs).coeff 0 = 1

The constant term of the Poincaré polynomial is 1: the identity is the unique element of length 0.

theorem TauCeti.poincarePolynomial_ne_zero {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] : poincarePolynomial cs ≠ 0

The Poincaré polynomial is nonzero.

@[simp]

theorem TauCeti.eval_one_poincarePolynomial {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] : Polynomial.eval 1 (poincarePolynomial cs) = ↑(Nat.card W)

The value at 1 is the order of the group: every element contributes 1.

@[simp]

theorem TauCeti.eval_neg_one_poincarePolynomial {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] [Nonempty B] : Polynomial.eval (-1) (poincarePolynomial cs) = 0

The Poincaré polynomial vanishes at -1 as soon as there is at least one simple reflection: left multiplication by it is a sign-reversing involution of W, so the terms of the alternating sum cancel in pairs.

Degree

theorem TauCeti.natDegree_poincarePolynomial {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] : IsGreatest (Set.range cs.length) (poincarePolynomial cs).natDegree

The degree of the Poincaré polynomial is the largest length occurring in W: it is attained by some element, and no element is longer.

theorem TauCeti.leadingCoeff_poincarePolynomial {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] : (poincarePolynomial cs).leadingCoeff = ↑(Nat.card { w : W // cs.length w = (poincarePolynomial cs).natDegree })

The leading coefficient counts the elements of maximal length.

Transport along a reindexing or a group isomorphism

@[simp]

theorem TauCeti.poincarePolynomial_reindex {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {B' : Type u_3} [Finite W] (e : B ≃ B') : poincarePolynomial (cs.reindex e) = poincarePolynomial cs

The Poincaré polynomial only depends on the Coxeter system up to relabelling the simple reflections, since the length function does (CoxeterSystem.length_reindex).

@[simp]

theorem TauCeti.poincarePolynomial_map {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {H : Type u_4} [Group H] [Finite W] [Finite H] (e : W ≃* H) : poincarePolynomial (cs.map e) = poincarePolynomial cs

The Poincaré polynomial is invariant under transporting the Coxeter system along a group isomorphism, since the length function is (CoxeterSystem.length_map). The hypothesis [Finite H] follows from [Finite W], but is needed to state the left-hand side.

The two smallest cases

@[simp]

theorem TauCeti.poincarePolynomial_of_isEmpty {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] [IsEmpty B] : poincarePolynomial cs = 1

The rank-zero case: with no simple reflections the group is trivial and the Poincaré polynomial is 1.

@[simp]

theorem TauCeti.poincarePolynomial_of_unique_index {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Finite W] [Unique B] : poincarePolynomial cs = 1 + Polynomial.X

The rank-one case: a Coxeter system with a single simple reflection has Poincaré polynomial 1 + q, its group being the two-element group generated by that reflection.