LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Type-A reduced words and the Coxeter presentation

Statement

Let $n \geq 2$ , let $S_{n}$ be the permutation group on ${1, \dots, n}$ with simple adjacent transpositions $s_{i} = (i i + 1)$ , and let a word in the $s_{i}$ be reduced when it has minimal length among words representing its permutation.

(a) Type-A braid connectivity. Any two reduced words for one $w \in S_{n}$ are related by finitely many commutations $s_{i} s_{j} \leftrightarrow s_{j} s_{i}$ for $∣ i - j ∣ > 1$ and adjacent braid moves $s_{i} s_{i + 1} s_{i} \leftrightarrow s_{i + 1} s_{i} s_{i + 1}$ .

(b) Coxeter presentation. The canonical evaluation homomorphism $Φ : ⟨ t_{1}, \dots, t_{n - 1} | t_{i}^{2} = 1, t_{i} t_{j} = t_{j} t_{i} (∣ i - j ∣ > 1), t_{i} t_{i + 1} t_{i} = t_{i + 1} t_{i} t_{i + 1} ⟩ ⟶ S_{n}, t_{i} ⟼ s_{i}$ is an isomorphism. In particular these are a complete set of relations among the adjacent transpositions, not merely relations they satisfy.

For $n = 0, 1$ both sides of the presentation have no generators and are trivial. No choice principle is used.

Facts & Assumptions

Given: The type-A presentation group $C_{n}$ displayed in (b), the ordinary permutation group $S_{n}$ , and words in their respective adjacent generators.

[F1]

In Reduced adjacent-transposition words have well-defined positive lifts, parts (a), (b), (c), (e), and (g) prove directly from permutations and inversion sets that the $s_{i}$ satisfy the involution, far-commutation, and adjacent braid relations; they generate $S_{n}$ ; a word is reduced exactly when its length is $inv$ of its permutation; multiplication on the right by $s_{i}$ changes $inv$ by exactly $+ 1$ or $- 1$ ; and any two reduced words for one permutation are connected by the two braid-move families. That item's proof imports only the exchange-to-Matsumoto induction from Dehornoy IX Corollary 1.11(ii) with its type-A hypotheses checked; it does not cite the published Coxeter-presentation theorem.

[F2]

If images of the generators satisfy every relator of a group presentation, the assignment extends uniquely to a homomorphism; it is surjective when those images generate the target (Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

[F3]

Induction on a natural-valued word length is valid (The principle of mathematical induction).

Proof

Proof technique: direct, with induction on the length of an arbitrary presentation word.

1.1

The evaluation map. By [F1] the permutations $s_{i}$ satisfy every relator displayed in (b), so [F2] gives a homomorphism $Φ : C_{n} \to S_{n}$ . It is surjective because the $s_{i}$ generate $S_{n}$ by [F1].

F1F2

2.1

Reduced-word connectivity (a). The braid-connectivity clause of [F1] gives exactly the two types of moves in (a). Each is also a relator of $C_{n}$ , so braid-equivalent reduced $s$ -words have equal corresponding $t$ -words in $C_{n}$ .

F1step 1.1

3.1

Reduction of every presentation word. We prove by induction on $k$ that every word of $k$ letters $t_{i}$ in $C_{n}$ equals a reduced $t$ -word for its image under $Φ$ . Every group word can first be put in this form: $t_{i}^{- 1} = t_{i}$ by the involution relator, so replace each inverse letter. For $k = 0$ the empty word is reduced for the identity. For the induction step write the word as $u t_{i}$ with $u$ of length $k - 1$ , and let $τ = Φ (u)$ and $σ = τ s_{i}$ . By induction $u$ equals a reduced $t$ -word $q$ for $τ$ . By [F1], either $inv (σ) = inv (τ) + 1$ or it is $inv (τ) - 1$ . If the inversion number increases, $q t_{i}$ is reduced for $σ$ by [F1], so it is the required representative. If it decreases, choose a reduced $s$ -word $r$ for $σ$ ; one exists because the $s_{i}$ generate $S_{n}$ and minimal finite word length exists. Since $σ s_{i} = τ$ and $inv (τ) = inv (σ) + 1$ , the word $r s_{i}$ is reduced for $τ$ by [F1]. Thus the two reduced words $q$ and $r s_{i}$ for $τ$ are braid-connected by step 2.1; replacing $s$ by $t$ gives $q = r t_{i}$ in $C_{n}$ . Consequently $u t_{i} = q t_{i} = r t_{i}^{2} = r$ in $C_{n}$ , and $r$ is reduced for $σ$ . This completes the induction.

F1F3step 2.1

4.1

Injectivity and the presentation (b). If $g \in \ker Φ$ , represent $g$ by a finite word and use step 3.1 to replace it in $C_{n}$ by a reduced word for the identity of $S_{n}$ . By [F1] the identity has inversion number zero, so its only reduced word is empty; hence $g = 1$ . Thus $Φ$ is injective, and with step 1.1 it is an isomorphism.

F1step 1.1step 3.1

5.1

Small ranks. For $n \leq 1$ there are no adjacent generators and $S_{n}$ is trivial, so the empty presentation is trivial as well. Every argument above uses only finite words and induction on their lengths. ∎

step 2.1step 4.1

Remarks

The injectivity step is the missing direction in the published thm-the-symmetric-group-has-the-coxeter-presentation: knowing that the $s_{i}$ satisfy the relators and generate $S_{n}$ proves only surjectivity. This local proof uses reduced-word connectivity and the involution relation to turn every presentation word into a reduced representative of its image.
The reduced-word result is taken through the earlier Garside type-A item [F1], whose exchange and inversion arguments do not use a Coxeter presentation. The present item therefore supplies the Coxeter-system interface needed by the Soergel source imports without depending on the pending published proof.

Depends on

Used by

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Elias–Williamson, Soergel Calculus, §2.1, PDF pp.13–14 (standard reference, not scraped)
Libedinsky, Gentle Introduction to Soergel Bimodules I, §3, PDF pp.11–13 (standard reference, not scraped)