Rank-two standard parabolic subgroups, and Tits' lemma

Let cs : CoxeterSystem M W and let i ≠ i' be two indices. The standard parabolic subgroup cs.parabolic {i, i'} is generated by the two involutions s i and s i', so it is a dihedral group, and the words that spell its elements are the alternating words of Mathlib's CoxeterSystem.alternatingWord. This file proves that, and extracts from it Tits' lemma: an element with two distinct left descents has a rank-two parabolic factor that is spelled by both alternating words of its length, and that length is exactly the order of the rotation s i * s i'.

Three steps carry the whole file.

• A reduced word has no two adjacent equal letters (CoxeterSystem.IsReduced.isChain_ne), because deleting such a pair shortens the word without changing its product. A list in two letters with no adjacent repetition is an alternating word (CoxeterSystem.eq_alternatingWord_of_forall_mem_pair), so a reduced word for an element of cs.parabolic {i, i'} is one of the two alternating words of its length.
• The two alternating words of a given length have the same product exactly when the rotation s i * s i' is killed by that length (CoxeterSystem.wordProd_alternatingWord_eq_comm_iff), and the alternating words repeat with period twice the order of that rotation (CoxeterSystem.wordProd_alternatingWord_add_two_mul). Both are direct computations from CoxeterSystem.prod_alternatingWord_eq_mul_pow, and they are the only place the dihedral arithmetic enters.
• A left descent i of w turns a reduced word for s i * w into a reduced word for w beginning with i. If both i and i' are left descents of a parabolic w, that produces two reduced words for w with different first letters, hence — the two alternating words being the only candidates — both alternating words of length ℓ w spell w.

Together these pin the length down: an element of cs.parabolic {i, i'} with both i and i' as left descents has length exactly orderOf (s i * s i') (CoxeterSystem.length_eq_orderOf_of_isLeftDescent_pair). The first two steps give that the order divides the length; periodicity keeps the length below twice the order, and divisibility then forces equality.

The order of the rotation against the Coxeter-matrix entry

Tits' lemma is classically stated with the Coxeter-matrix entry M i i' in place of the order of the rotation. The two do agree — that is Tits' theorem on the geometric representation of a Coxeter system — but the defining relations of M give only the divisibility orderOf (s i * s i') ∣ M i i' (CoxeterSystem.simple_mul_simple_pow). So the statements below are phrased with orderOf (s i * s i'), which is what the dihedral combinatorics determines on its own, and CoxeterSystem.length_le_of_isLeftDescent_pair records the bound by M i i' that the divisibility yields.

The exactness orderOf (s i * s i') = M i i' is what separates these statements from the induction step of Matsumoto's theorem: a braid move rewrites an alternating word of length M i i', so turning Tits' lemma into two braid-equivalent reduced words for w, one beginning with i and one with i', needs the rank-two parabolic factor to have length M i i' on the nose.

Main results

• CoxeterSystem.eq_alternatingWord_of_forall_mem_pair and CoxeterSystem.eq_alternatingWord_or_of_forall_mem_pair: a list in two letters with no adjacent repetition is an alternating word.
• CoxeterSystem.wordProd_alternatingWord_eq_of_mem_parabolic_pair: every element of a rank-two standard parabolic subgroup is spelled by an alternating word of its own length.
• CoxeterSystem.wordProd_alternatingWord_eq_comm_iff: the two alternating words of length m have the same product exactly when (s i * s i') ^ m = 1.
• CoxeterSystem.wordProd_alternatingWord_eq_mul_pow: more precisely, they differ by the factor (s i * s i') ^ m.
• CoxeterSystem.wordProd_alternatingWord_add_two_mul: the products of the alternating words repeat with period twice the order of s i * s i'.
• CoxeterSystem.wordProd_alternatingWord_eq_of_isLeftDescent_pair: an element of a rank-two standard parabolic subgroup with two distinct left descents is spelled by both alternating words of its length, hence CoxeterSystem.pow_length_eq_one_of_isLeftDescent_pair and CoxeterSystem.length_eq_orderOf_of_isLeftDescent_pair: that length is the order of s i * s i', and so at most M i i' (CoxeterSystem.length_le_of_isLeftDescent_pair).
• CoxeterSystem.exists_mem_parabolic_pair_mul_of_isLeftDescent_pair: the rank-two parabolic factor of an element with two distinct left descents inherits both descents.
• CoxeterSystem.exists_wordProd_alternatingWord_mul_of_isLeftDescent_pair: Tits' lemma.

References

• A. Björner and F. Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), Sections 2.2 and 3.3.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Sections 1.9 and 5.12.

Words in two letters

theorem CoxeterSystem.eq_alternatingWord_of_forall_mem_pair {B : Type u_1} {i i' : B} {ω : List B} (hmem : ∀ j ∈ ω, j = i ∨ j = i') (hchain : List.IsChain (fun (x1 x2 : B) => x1 ≠ x2) ω) (hlast : ∀ j ∈ ω.getLast?, j = i') : ω = alternatingWord i i' ω.length

A list in two letters with no adjacent repetition is an alternating word. If every letter of ω is i or i', no two adjacent letters are equal, and the last letter is i', then ω is the alternating word of its own length ending in i'.

theorem CoxeterSystem.eq_alternatingWord_or_of_forall_mem_pair {B : Type u_1} {i i' : B} {ω : List B} (hmem : ∀ j ∈ ω, j = i ∨ j = i') (hchain : List.IsChain (fun (x1 x2 : B) => x1 ≠ x2) ω) : ω = alternatingWord i i' ω.length ∨ ω = alternatingWord i' i ω.length

A list in two letters with no adjacent repetition is one of the two alternating words of its length. Which of the two it is, is decided by its last letter.

Elements of a rank-two standard parabolic subgroup

theorem CoxeterSystem.eq_alternatingWord_or_of_isReduced {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} {ω : List B} (hω : cs.IsReduced ω) (hmem : ∀ j ∈ ω, j = i ∨ j = i') : ω = alternatingWord i i' ω.length ∨ ω = alternatingWord i' i ω.length

A reduced word all of whose letters are i or i' is one of the two alternating words of its length.

theorem CoxeterSystem.wordProd_alternatingWord_eq_of_mem_parabolic_pair {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} {w : W} (hw : w ∈ cs.parabolic {i, i'}) : cs.wordProd (alternatingWord i i' (cs.length w)) = w ∨ cs.wordProd (alternatingWord i' i (cs.length w)) = w

Every element of a rank-two standard parabolic subgroup is spelled by an alternating word of its own length. Being of length ℓ w, that word is reduced.

theorem CoxeterSystem.wordProd_alternatingWord_eq_mul_pow {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (m : ℕ) : cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i m) * (cs.simple i * cs.simple i') ^ m

The two alternating words of length m differ by the m-th power of the rotation. The word alternating between i and i' and ending with i' is the word ending with i followed by (s i * s i') ^ m.

theorem CoxeterSystem.wordProd_alternatingWord_eq_comm_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (m : ℕ) : cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i m) ↔ (cs.simple i * cs.simple i') ^ m = 1

The two alternating words of length m have the same product exactly when the rotation s i * s i' is killed by m. This is the dihedral arithmetic of a rank-two parabolic subgroup.

theorem CoxeterSystem.wordProd_alternatingWord_add_two_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) {n : ℕ} (hn : (cs.simple i * cs.simple i') ^ n = 1) (m : ℕ) : cs.wordProd (alternatingWord i i' (m + 2 * n)) = cs.wordProd (alternatingWord i i' m)

The products of the alternating words repeat with period twice the order of the rotation s i * s i'. Only (s i * s i') ^ n = 1 is used, so the period may be read off any exponent killing the rotation.

Two left descents

theorem CoxeterSystem.wordProd_alternatingWord_eq_of_isLeftDescent_pair {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} (hne : i ≠ i') {w : W} (hw : w ∈ cs.parabolic {i, i'}) (hd : cs.IsLeftDescent w i) (hd' : cs.IsLeftDescent w i') : cs.wordProd (alternatingWord i i' (cs.length w)) = w ∧ cs.wordProd (alternatingWord i' i (cs.length w)) = w

An element of a rank-two standard parabolic subgroup with two distinct left descents is spelled by both alternating words of its length. The two descents produce two reduced words with different first letters, and the two alternating words of that length are the only candidates.

theorem CoxeterSystem.pow_length_eq_one_of_isLeftDescent_pair {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} (hne : i ≠ i') {w : W} (hw : w ∈ cs.parabolic {i, i'}) (hd : cs.IsLeftDescent w i) (hd' : cs.IsLeftDescent w i') : (cs.simple i * cs.simple i') ^ cs.length w = 1

The rotation s i * s i' is killed by the length of an element of cs.parabolic {i, i'} with two distinct left descents.

theorem CoxeterSystem.length_eq_orderOf_of_isLeftDescent_pair {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} (hne : i ≠ i') {w : W} (hw : w ∈ cs.parabolic {i, i'}) (hd : cs.IsLeftDescent w i) (hd' : cs.IsLeftDescent w i') : cs.length w = orderOf (cs.simple i * cs.simple i')

An element of cs.parabolic {i, i'} with two distinct left descents has length exactly the order of the rotation s i * s i'. The order divides the length by CoxeterSystem.pow_length_eq_one_of_isLeftDescent_pair; were the length at least twice the order, the periodicity of the alternating words would spell w by a strictly shorter word.

theorem CoxeterSystem.length_le_of_isLeftDescent_pair {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} (hne : i ≠ i') (hM : M.M i i' ≠ 0) {w : W} (hw : w ∈ cs.parabolic {i, i'}) (hd : cs.IsLeftDescent w i) (hd' : cs.IsLeftDescent w i') : cs.length w ≤ M.M i i'

An element of cs.parabolic {i, i'} with two distinct left descents is no longer than the Coxeter-matrix entry M i i': its length is the order of s i * s i', which divides M i i'.

theorem CoxeterSystem.exists_mem_parabolic_pair_mul_of_isLeftDescent_pair {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} {w : W} (hd : cs.IsLeftDescent w i) (hd' : cs.IsLeftDescent w i') : ∃ (x : W) (v : W), x ∈ cs.parabolic {i, i'} ∧ cs.IsLeftDescent x i ∧ cs.IsLeftDescent x i' ∧ w = x * v ∧ cs.length w = cs.length x + cs.length v

The rank-two parabolic factor of an element with two distinct left descents inherits both descents. The factorization is the one of CoxeterSystem.existsUnique_mem_parabolic_mul, whose lengths add.

theorem CoxeterSystem.exists_wordProd_alternatingWord_mul_of_isLeftDescent_pair {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} (hne : i ≠ i') {w : W} (hd : cs.IsLeftDescent w i) (hd' : cs.IsLeftDescent w i') : ∃ (v : W), 0 < orderOf (cs.simple i * cs.simple i') ∧ w = cs.wordProd (alternatingWord i i' (orderOf (cs.simple i * cs.simple i'))) * v ∧ w = cs.wordProd (alternatingWord i' i (orderOf (cs.simple i * cs.simple i'))) * v ∧ cs.length w = orderOf (cs.simple i * cs.simple i') + cs.length v

Tits' lemma. If i ≠ i' are both left descents of w, then w splits as a rank-two parabolic factor times a remainder, the lengths adding, and the parabolic factor is spelled by both alternating words of length orderOf (s i * s i').

Classically the exponent is the Coxeter-matrix entry M i i'; the order of s i * s i' divides it (CoxeterSystem.simple_mul_simple_pow), which gives the bound CoxeterSystem.length_le_of_isLeftDescent_pair, and the two agree by Tits' theorem on the geometric representation — see the module docstring.