TheoremStatement: 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.

The standard basis of the generic Hecke algebra and base change

Statement

Let $(S, m)$ , $W$ , $ℓ$ be as in Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups; let $R$ , $v_{s}$ , $H$ , $T_{s}$ be as in Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy; let $T_{w}$ for $w \in W$ and the spanning statement be as in Reduced-word independence of T_w and the length-multiplication rules; and let $E$ , $P_{s}$ , $Q_{s}$ and $P_{w}$ be as in The commuting left and right length operators and their Hecke relations.

The length-operator representation. There is a unique unital $R$ -algebra homomorphism $ρ : H \to {End}_{R} (E)$ with $ρ (T_{s}) = P_{s}$ for all $s \in S$ ; it satisfies $ρ (T_{w}) = P_{w}$ and $ρ (T_{w}) (e_{1}) = e_{w}$ for all $w \in W$ .
Standard basis. ${T_{w} : w \in W}$ is an $R$ -basis of $H$ : it spans by Reduced-word independence of T_w and the length-multiplication rules and is $R$ -linearly independent. Hence $H$ is free as an $R$ -module and every element of $H$ has a unique expansion $\sum_{w} a_{w} T_{w}$ with $a_{w} \in R$ and all but finitely many $a_{w}$ zero.
Faithfulness. $ρ$ is injective.
Base change. For every commutative ring $R^{'}$ and every ring homomorphism $φ : R \to R^{'}$ , the scalar extension $R^{'} \otimes_{R} H$ is, as an $R^{'}$ -algebra, canonically isomorphic to the quotient of the free associative $R^{'}$ -algebra on $(T_{s})_{s \in S}$ by the two-sided ideal generated by the images under $φ$ of the relations (Q) and (B) of Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy, and it is free as an $R^{'}$ -module with basis $(1 \otimes T_{w})_{w \in W}$ . No flatness or freeness of $R^{'}$ over $R$ is assumed, and no torsion-freeness or semisimplicity of $H$ or of its specialisations is claimed.

Facts & Assumptions

Given: A finite Coxeter matrix $(S, m)$ , the group $W$ with length $ℓ$ , the parameters $R$ , $v_{s}$ and the algebra $H$ , and the free $R$ -module $E$ with basis $(e_{w})_{w \in W}$ and operators $P_{s}$ , $Q_{s}$ , $P_{w}$ .

[F1]

The operators satisfy $P_{s}^{2} = (v_{s} - v_{s}^{- 1}) P_{s} + {id}_{E}$ , the braid relations $P_{s} P_{t} P_{s} \dots = P_{t} P_{s} P_{t} \dots$ of $m (s, t)$ alternating factors for $s \neq t$ with $m (s, t) < \infty$ , and $P_{s} Q_{t} = Q_{t} P_{s}$ ; for a reduced expression $w = s_{1} \dots s_{k}$ the product $P_{w} : = P_{s_{1}} \dots P_{s_{k}}$ is independent of the reduced expression and satisfies $P_{w} (e_{1}) = e_{w}$ . (The commuting left and right length operators and their Hecke relations)

[F2]

$H = F / I$ is presented by the generators $T_{s}$ subject to the relations (Q) $(T_{s} - v_{s}) (T_{s} + v_{s}^{- 1}) = 0$ and (B) the alternating braid equalities; consequently, for every unital associative $R$ -algebra $A$ and every family $(t_{s})$ in $A$ satisfying (Q) and (B) there is a unique unital $R$ -algebra homomorphism $H \to A$ with $T_{s} \mapsto t_{s}$ . (Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy)

[F3]

For a reduced expression $w = s_{1} \dots s_{k}$ the element $T_{w} : = T_{s_{1}} \dots T_{s_{k}}$ is well defined and independent of the reduced expression, and ${T_{w} : w \in W}$ spans $H$ as an $R$ -module. (Reduced-word independence of T_w and the length-multiplication rules)

[F4]

In a free module with basis $(e_{w})$ , the basis vectors are $R$ -linearly independent: a finite relation $\sum_{w} a_{w} e_{w} = 0$ has all $a_{w} = 0$ . (The free module on a set and its standard basis)

[F5]

${End}_{R} (E)$ is the endomorphism ring of $E$ , a unital ring under composition with central $R$ -action, and a unital $R$ -algebra homomorphism is multiplicative and unital. (The endomorphism ring ${End}_{R} (M)$ under addition and composition, Module endomorphisms form a ring under pointwise addition and composition, Algebras over a commutative ring, central structure maps, and algebra homomorphisms)

[F6]

For a commutative ring homomorphism $φ : R \to R^{'}$ , part 2 of Presentation base change and transport of explicit bases to commutative specializations identifies $R^{'} \otimes_{R} (R ⟨ X ⟩ / I)$ with $(R^{'} \otimes_{R} R ⟨ X ⟩) / im (R^{'} \otimes_{R} I)$ , the image ideal being generated by the images of the relations, with no flatness or freeness of $R^{'}$ over $R$ assumed; part 3 gives that tensoring a free $R$ -module with basis $(a_{i})$ yields a free $R^{'}$ -module with basis $(1 \otimes a_{i})$ .

Proof

Given: A finite Coxeter matrix $(S, m)$ , the group $W$ with length $ℓ$ , the algebra $H$ over $R$ , the free module $E$ with basis $(e_{w})_{w \in W}$ and the operators $P_{s}$ , $Q_{s}$ , $P_{w}$ .

1.1F1F2F5

By [F1] the operators $P_{s}$ satisfy the quadratic relations (Q) of [F2] and the braid relations (B). The family $(P_{s})_{s \in S}$ therefore lies in the unital associative $R$ -algebra ${End}_{R} (E)$ and satisfies the two families of relations (Q) and (B), so the universal property [F2] gives a unique unital $R$ -algebra homomorphism $ρ : H \to {End}_{R} (E)$ with $ρ (T_{s}) = P_{s}$ .

2.1F1F3F5step 1.1

For a reduced expression $w = s_{1} \dots s_{k}$ of $w$ , multiplicativity of $ρ$ ([F5]) and $T_{w} = T_{s_{1}} \dots T_{s_{k}}$ ([F3]) give $ρ (T_{w}) = ρ (T_{s_{1}}) \dots ρ (T_{s_{k}}) = P_{s_{1}} \dots P_{s_{k}}$ , which equals $P_{w}$ by [F1]; hence $ρ (T_{w}) (e_{1}) = P_{w} (e_{1}) = e_{w}$ ([F1]).

3.1F3F4step 2.1

Let $\sum_{w} a_{w} T_{w} = 0$ be a finite $R$ -linear relation in $H$ . Applying the $R$ -linear map $ρ$ and evaluating at $e_{1}$ gives $0 = ρ (\sum_{w} a_{w} T_{w}) (e_{1}) = \sum_{w} a_{w} ρ (T_{w}) (e_{1}) = \sum_{w} a_{w} e_{w}$ by step 2.1, so $a_{w} = 0$ for all $w$ by the linear independence of the basis $(e_{w})$ ([F4]). Thus ${T_{w}}$ is $R$ -linearly independent; combined with the spanning statement of [F3] it is an $R$ -basis, so $H$ is free and each element has a unique expansion as stated.

4.1F4step 2.1step 3.1

If $ρ (h) = 0$ , write $h = \sum_{w} a_{w} T_{w}$ in its unique expansion from step 3.1; then $0 = ρ (h) (e_{1}) = \sum_{w} a_{w} ρ (T_{w}) (e_{1}) = \sum_{w} a_{w} e_{w}$ by step 2.1, so $a_{w} = 0$ for all $w$ and $h = 0$ . Hence $ρ$ is injective.

4.2F3F6step 3.1

Since ${T_{w}}$ is an $R$ -basis of $H$ (step 3.1), [F6] part 2 identifies $R^{'} \otimes_{R} H$ with the quotient of $R^{'} \otimes_{R} R ⟨ T_{s} : s \in S ⟩$ by the ideal generated by the images of (Q) and (B), and part 1 of Presentation base change and transport of explicit bases to commutative specializations identifies the latter free algebra with the free associative $R^{'}$ -algebra on $(T_{s})_{s \in S}$ ; by [F6] part 3, applied to the free $R$ -module $H$ with basis $(T_{w})$ , the scalar extension is free with basis $(1 \otimes T_{w})_{w \in W}$ . All of this holds for an arbitrary ring homomorphism $φ$ , with no flatness, torsion-freeness or semisimplicity hypothesis.

5.1F1step 1.1step 2.1step 3.1step 4.1step 4.2∎

Assembly: part 1 is step 1.1 together with step 2.1, part 2 is step 3.1, part 3 is step 4.1 and part 4 is step 4.2. No choice is used: the construction selects no objects beyond the given data, the operators are defined by explicit length conditions ([F1]), and the only "evaluation" is at the explicitly named vector $e_{1}$ .

Depends on

Used by

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

Dependency tree · two levels

49 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)