LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

Reduced-word independence of T_w and the length-multiplication rules

Statement

Let $(S, m)$ , $W$ , $ℓ$ be as in Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, and let $R$ , $v_{s}$ , $H$ and the generators $T_{s}$ be as in Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy.

Well-defined reduced products. If $w = s_{1} \dots s_{k}$ and $w = s_{1}^{'} \dots s_{k}^{'}$ are reduced expressions of $w \in W$ (so $k = ℓ (w)$ ), then $T_{s_{1}} \dots T_{s_{k}} = T_{s_{1}^{'}} \dots T_{s_{k}^{'}} in H .$ Hence $T_{w} : = T_{s_{1}} \dots T_{s_{k}}$ is a well-defined element of $H$ depending only on $w$ ; in particular $T_{1} = 1$ (the empty product).
Length-multiplication rules. For all $s \in S$ and $w \in W$ , $T_{s} T_{w} = {\begin{cases} T_{s w}, & ℓ (s w) = ℓ (w) + 1, \\ T_{s w} + (v_{s} - v_{s}^{- 1}) T_{w}, & ℓ (s w) = ℓ (w) - 1, \end{cases} T_{w} T_{s} = {\begin{cases} T_{w s}, & ℓ (w s) = ℓ (w) + 1, \\ T_{w s} + (v_{s} - v_{s}^{- 1}) T_{w}, & ℓ (w s) = ℓ (w) - 1. \end{cases}$ (Exactly one case occurs, by Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action, part 1.)
Spanning. Every product $T_{s_{1}} \dots T_{s_{k}}$ of generators is a finite $R$ -linear combination of the elements $T_{w}$ , and consequently ${T_{w} : w \in W}$ spans $H$ as an $R$ -module: every element of $H$ is a finite sum $\sum_{w} a_{w} T_{w}$ with $a_{w} \in R$ .
Scope. No independence or freeness of ${T_{w}}$ is asserted here; that is The standard basis of the generic Hecke algebra and base change.

Facts & Assumptions

Given: A finite Coxeter matrix $(S, m)$ , the group $W$ with length $ℓ$ , and the presented algebra $H$ with generators $T_{s}$ and coefficient ring $R$ .

[F1]

Any two reduced expressions of the same $w \in W$ are braid-equivalent: one is obtained from the other by finitely many replacements of an alternating subword $s t s t \dots$ of length $m (s, t) < \infty$ by the alternating word $t s t s \dots$ of the same length. (Matsumoto's theorem: braid connectivity of reduced expressions, with singleton detection in dihedral subgroups)

[F2]

$H$ is the quotient of the free associative $R$ -algebra $F = R ⟨ T_{s} : s \in S ⟩$ by the two-sided ideal generated by the relations $(T_{s} - v_{s}) (T_{s} + v_{s}^{- 1}) = 0$ and, for $s \neq t$ with $m (s, t) < \infty$ , the equality of the two alternating products of $m (s, t)$ factors; in particular those two products are equal in $H$ , and $T_{s}^{2} = (v_{s} - v_{s}^{- 1}) T_{s} + 1$ in $H$ . (Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy)

[F3]

For all $x \in W$ and $s \in S$ one has $ℓ (s x) = ℓ (x) \pm 1$ and $ℓ (x s) = ℓ (x) \pm 1$ . (Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action)

[F4]

$ℓ (w)$ is the least length of a word in $S$ representing $w$ , so a word of length $ℓ (w)$ representing $w$ is a reduced expression, and a multiplicative identity $w = w^{'} \cdot s$ with $ℓ (w) = ℓ (w^{'}) + 1$ together with a reduced expression of $w^{'}$ yields a reduced expression of $w$ by concatenation. (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups)

[F5]

$F$ is free as an $R$ -module on the finite words in the generators, so every element of $F$ , and hence every element of the quotient $H$ , is a finite $R$ -linear combination of images of words. (The free associative R-algebra on a set and descent of relations)

[F6]

The induction principle holds: a property of natural numbers holding at $0$ and stable under successors holds for all natural numbers. (The principle of mathematical induction, The natural numbers $N$ (von Neumann))

Proof

Given: A finite Coxeter matrix $(S, m)$ , the group $W$ with length $ℓ$ , and the presented algebra $H$ over $R$ .

1.1F1F2

If $w = s_{1} \dots s_{k}$ and $w = s_{1}^{'} \dots s_{k}^{'}$ are reduced expressions, then by [F1] they are connected by finitely many braid moves. A braid move replaces a consecutive block $s, t, s, \dots$ of $m (s, t)$ alternating letters by $t, s, t, \dots$ , and the corresponding block $T_{s} T_{t} T_{s} \dots$ of the product is replaced by $T_{t} T_{s} T_{t} \dots$ , which equals it in $H$ by the braid relation ([F2]); letters outside the block are untouched. Reading the moves one at a time, the two products are equal, so $T_{w} : = T_{s_{1}} \dots T_{s_{k}}$ is a well-defined element of $H$ ; for $w = 1$ the empty product equals $1$ .

2.1F3F4step 1.1

Suppose $ℓ (s w) = ℓ (w) + 1$ and let $w = s_{1} \dots s_{k}$ be a reduced expression, so $k = ℓ (w)$ . Then $s s_{1} \dots s_{k}$ is a word of length $ℓ (w) + 1 = ℓ (s w)$ representing $s w$ , hence a reduced expression of $s w$ ([F4]), and the definition of $T_{s w}$ from 1.1 gives $T_{s w} = T_{s} T_{s_{1}} \dots T_{s_{k}} = T_{s} T_{w}$ . Similarly, if $ℓ (w s) = ℓ (w) + 1$ , then appending $s$ to a reduced expression of $w$ gives a reduced expression of $w s$ , so $T_{w s} = T_{w} T_{s}$ .

3.1F2F3step 2.1

Suppose $ℓ (s w) = ℓ (w) - 1$ and put $w^{'} : = s w$ , so that $s w^{'} = w$ and $ℓ (s w^{'}) = ℓ (w) = ℓ (w^{'}) + 1$ ([F3]). By 2.1, $T_{w} = T_{s w^{'}} = T_{s} T_{w^{'}}$ . Multiplying the quadratic relation $T_{s}^{2} = (v_{s} - v_{s}^{- 1}) T_{s} + 1$ of [F2] on the right by $T_{w^{'}}$ gives $T_{s}^{2} T_{w^{'}} = (v_{s} - v_{s}^{- 1}) T_{s} T_{w^{'}} + T_{w^{'}}$ , that is $T_{s} T_{w} = T_{s w} + (v_{s} - v_{s}^{- 1}) T_{w}$ . The right-handed rule follows by multiplying the same relation on the left by $T_{w^{'}}$ with $w^{'} = w s$ .

4.1F2F5F6step 1.1step 2.1step 3.1

By [F5] every element of $H$ is a finite $R$ -linear combination of images of words in the $T_{s}$ , so it suffices to show that every word product $T_{s_{1}} \dots T_{s_{k}}$ is a finite $R$ -linear combination of the $T_{w}$ . Argue by induction on $k$ ([F6]): for $k = 0$ the empty product is $T_{1}$ by 1.1, and for $k \geq 1$ the induction hypothesis writes $T_{s_{2}} \dots T_{s_{k}}$ as a finite $R$ -linear combination of the $T_{w}$ , after which left multiplication by $T_{s_{1}}$ distributes and step 2.1 or step 3.1 expresses each $T_{s_{1}} T_{w}$ as an $R$ -linear combination of $T_{s_{1} w}$ and $T_{w}$ (with $s_{1} w$ a group element, so $T_{s_{1} w}$ is among the $T$ 's). This gives the spanning claim.

5.1F4step 1.1step 2.1step 3.1step 4.1∎

Combining the steps: 1.1 gives the well-definedness of $T_{w}$ including $T_{1} = 1$ , steps 2.1 and 3.1 give the two multiplication rules in both hands, and step 4.1 gives spanning. Nothing here asserts independence or freeness of ${T_{w}}$ ; that is the content of The standard basis of the generic Hecke algebra and base change. No choice is used and $W$ need not be finite: reduced expressions are supplied by the minimum in the definition of $ℓ$ ([F4]) and the induction of step 4.1 runs over finite words.

Depends on

Used by

Cited to discharge well-definedness by Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy.

Dependency tree · two levels

58 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

George Lusztig, Lectures on Hecke Algebras with Unequal Parameters (MIT Fall 1999 lecture notes, arXiv:math/0108172v1) (standard reference, not scraped)
Meinolf Geck, Modular Representations of Hecke Algebras (EPFL course notes, arXiv:math/0511548v2) (standard reference, not scraped)
Anders Bjorner and Francesco Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), complete book PDF (standard reference, not scraped)