The symmetric group as the Coxeter group of type A

The symmetric group on n letters is the Coxeter group of type A_{n-1}: with the adjacent transpositions s i = (i i+1), i < n - 1, as simple reflections, Equiv.Perm (Fin n) is presented by the Coxeter matrix CoxeterMatrix.A (n - 1). This file constructs that Coxeter system, TauCeti.permCoxeterSystem n, and identifies its combinatorics:

• a simple reflection s i is a right descent of σ exactly when σ reverses the order of the two letters i and i + 1;
• the Coxeter length of σ is its number of inversions, the pairs x < y with σ y < σ x;
• a Coxeter element, a product of all the adjacent transpositions each taken once in any order, is an n-cycle, so the Coxeter number of type A_{n-1} is n. In the natural order the product s 0 * s 1 * ⋯ * s (n - 2) is the cycle (0 1 ⋯ n-1).

The indexing follows TauCeti.BraidGroup: the simple reflection s i is TauCeti.BraidGroup.transposition i, which swaps the strands TauCeti.BraidGroup.strand i and TauCeti.BraidGroup.strandSucc i, so that the canonical map from the braid group onto this Coxeter group is the strand permutation TauCeti.BraidGroup.permHom.

With the Coxeter system in place, the general Coxeter theory applies to permutations: reduced words and the length API of Mathlib.GroupTheory.Coxeter.Length, and Matsumoto's theorem TauCeti.matsumoto, which evaluates braid-relation-satisfying generators of any monoid along reduced words of a permutation. That is the form in which the standard basis T_w of a type-A Iwahori–Hecke algebra is defined.

Main definitions

• TauCeti.permCoxeterSystem n: the Coxeter system of type A_{n-1} on Equiv.Perm (Fin n).

Main results

• TauCeti.permCoxeterSystem_simple: its simple reflections are the adjacent transpositions.
• TauCeti.isRightDescent_permCoxeterSystem_iff and TauCeti.isLeftDescent_permCoxeterSystem_iff: descents are the reversed adjacent pairs of σ and of σ⁻¹.
• TauCeti.permCoxeterSystem_length_eq_card_inversion: the Coxeter length is the number of inversions.
• Equiv.Perm.permCoxeterSystem_length_decomposeFin'Symm: inserting i at the first position adds i to the Coxeter length.
• TauCeti.isCycle_wordProd_permCoxeterSystem, TauCeti.cycleType_wordProd_permCoxeterSystem and TauCeti.orderOf_wordProd_permCoxeterSystem: every Coxeter element is a cycle through all n letters, of order n.
• TauCeti.permCoxeterSystem_wordProd_finRange: the Coxeter element in the natural order is finRotate n.
• TauCeti.BraidGroup.permHom_eq_toCoxeterGroup: the strand permutation of a braid is the canonical map from the Artin group of type A onto its Coxeter group.

Implementation notes

The Coxeter system is produced by CoxeterSystem.ofExchange, the characterization of Coxeter systems by the exchange condition. The exchange condition for adjacent transpositions comes from one observation: along a word s_{a₁} ⋯ s_{aₖ} for σ, follow the two values taken at the letters i and i + 1 by the suffix products s_{aⱼ} ⋯ s_{aₖ}. An adjacent transposition reverses the relative order of exactly one pair of values, so if σ reverses the order of i and i + 1, some letter s_{aⱼ} reverses that pair, and deleting it spells σ * s i.

That a Coxeter element is an n-cycle is proved for all orderings at once, by induction on k: a word using each of s 0, …, s (k - 1) exactly once spells a cycle through the letters 0, …, k. Cutting a word that uses each of s 0, …, s k once at its letter s k writes it as a * s k * b, which is conjugate by a to s k * (b * a). The word for b * a uses each of s 0, …, s (k - 1) once, so it spells a cycle through 0, …, k, and composing with s k, the transposition of k with the new letter k + 1, inserts k + 1 into that cycle.

References

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

noncomputable def TauCeti.permCoxeterSystem (n : ℕ) : CoxeterSystem (CoxeterMatrix.A (n - 1)) (Equiv.Perm (Fin n))

The symmetric group Equiv.Perm (Fin n) as the Coxeter group of type A_{n-1}, with the adjacent transpositions TauCeti.BraidGroup.transposition i as simple reflections.

@[simp]

theorem TauCeti.permCoxeterSystem_simple {n : ℕ} (i : Fin (n - 1)) : (permCoxeterSystem n).simple i = BraidGroup.transposition i

The simple reflections of the type-A Coxeter system on Equiv.Perm (Fin n) are the adjacent transpositions.

@[simp]

theorem TauCeti.permCoxeterSystem_wordProd {n : ℕ} (ω : List (Fin (n - 1))) : (permCoxeterSystem n).wordProd ω = (List.map BraidGroup.transposition ω).prod

A word in the type-A Coxeter system on Equiv.Perm (Fin n) spells the product of the corresponding adjacent transpositions.

theorem TauCeti.isRightDescent_permCoxeterSystem_iff {n : ℕ} {σ : Equiv.Perm (Fin n)} {i : Fin (n - 1)} : (permCoxeterSystem n).IsRightDescent σ i ↔ σ (BraidGroup.strandSucc i) < σ (BraidGroup.strand i)

Right descents of a permutation. The simple reflection s i is a right descent of σ exactly when σ reverses the order of the letters i and i + 1.

theorem TauCeti.isLeftDescent_permCoxeterSystem_iff {n : ℕ} {σ : Equiv.Perm (Fin n)} {i : Fin (n - 1)} : (permCoxeterSystem n).IsLeftDescent σ i ↔ σ⁻¹ (BraidGroup.strandSucc i) < σ⁻¹ (BraidGroup.strand i)

Left descents of a permutation. The simple reflection s i is a left descent of σ exactly when σ⁻¹ reverses the order of the letters i and i + 1.

theorem TauCeti.permCoxeterSystem_length_eq_card_inversion {n : ℕ} (σ : Equiv.Perm (Fin n)) : (permCoxeterSystem n).length σ = {p : Fin n × Fin n | p.1 < p.2 ∧ σ p.2 < σ p.1}.card

The Coxeter length of a permutation is its number of inversions, the pairs of letters x < y with σ y < σ x.

Coxeter elements

theorem TauCeti.isCycle_wordProd_permCoxeterSystem {n : ℕ} {ω : List (Fin (n - 1))} (hω : ω.Perm (List.finRange (n - 1))) (hn : 2 ≤ n) : ((permCoxeterSystem n).wordProd ω).IsCycle

A Coxeter element of S_n is an n-cycle. A product of all the adjacent transpositions, each taken once in any order, is a cycle.

theorem TauCeti.support_wordProd_permCoxeterSystem {n : ℕ} {ω : List (Fin (n - 1))} (hω : ω.Perm (List.finRange (n - 1))) (hn : 2 ≤ n) : ((permCoxeterSystem n).wordProd ω).support = Finset.univ

A Coxeter element of S_n, for n ≥ 2, moves every letter.

theorem TauCeti.cycleType_wordProd_permCoxeterSystem {n : ℕ} {ω : List (Fin (n - 1))} (hω : ω.Perm (List.finRange (n - 1))) (hn : 2 ≤ n) : ((permCoxeterSystem n).wordProd ω).cycleType = {n}

The cycle type of a Coxeter element of S_n, for n ≥ 2, is {n}.

theorem TauCeti.sameCycle_wordProd_permCoxeterSystem {n : ℕ} {ω : List (Fin (n - 1))} (hω : ω.Perm (List.finRange (n - 1))) (x y : Fin n) : ((permCoxeterSystem n).wordProd ω).SameCycle x y

Any two letters lie in the same cycle of a Coxeter element of S_n.

theorem TauCeti.orderOf_wordProd_permCoxeterSystem {n : ℕ} {ω : List (Fin (n - 1))} (hω : ω.Perm (List.finRange (n - 1))) (hn : n ≠ 0) : orderOf ((permCoxeterSystem n).wordProd ω) = n

The Coxeter number of type A_{n-1} is n. Every Coxeter element of S_n, a product of all the adjacent transpositions each taken once in any order, has order n.

theorem TauCeti.permCoxeterSystem_wordProd_finRange {n : ℕ} : (permCoxeterSystem n).wordProd (List.finRange (n - 1)) = finRotate n

The Coxeter cycle of S_n. The Coxeter element s 0 * s 1 * ⋯ * s (n - 2), the product of the adjacent transpositions in their natural order, is the cycle (0 1 ⋯ n-1), that is finRotate n : i ↦ i + 1 modulo n.

@[simp]

theorem Equiv.Perm.permCoxeterSystem_length_decomposeFin'Symm {n : ℕ} (σ : Perm (Fin (n + 1))) (i : Fin (n + 2)) : (TauCeti.permCoxeterSystem (n + 2)).length (decomposeFin'Symm i σ) = ↑i + (TauCeti.permCoxeterSystem (n + 1)).length σ

The length of the permutation obtained by inserting i at the first position is i plus the length of the original permutation.

theorem TauCeti.BraidGroup.permHom_eq_toCoxeterGroup (n : ℕ) : permHom n = ArtinGroup.toCoxeterGroup (permCoxeterSystem n)

The strand permutation of a braid is the canonical map from the Artin group of type A onto its Coxeter group, realized as the symmetric group.