LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 extended Iwahori–Matsumoto basis

Statement

Let $H_{I M} (R, q) = H_{a f f} (R, q) ⋊ Ω$ be the Iwahori–Matsumoto algebra of The Iwahori–Matsumoto affine Hecke algebra of a based root datum. For $w \in W_{a f f}$ , let $T_{w}$ be the product along a reduced expression, and let $U_{ω}$ denote the length-zero symmetry corresponding to $ω \in Ω$ . Then

{T_{w} U_{ω} : w \in W_{a f f}, ω \in Ω}

is a $C$ -basis of $H_{I M} (R, q)$ .

Facts & Assumptions

Given: The reduced based root datum, affine Coxeter system, positive conjugacy-invariant parameter function, and extended algebra from The Iwahori–Matsumoto affine Hecke algebra of a based root datum.

[F1]

The affine Coxeter group $W_{a f f}$ has finite simple set $S_{a f f}$ . For $s \in S_{a f f}$ , put $v_{s} = \sqrt{q_{s}} > 0$ and $N_{s} = v_{s}^{- 1} T_{s}$ . These normalized generators satisfy the symmetric quadratic relation. They satisfy the generic Coxeter braid relations: an even braid has equal numbers of each generator on its two sides; if $m (s, t) = 2 r + 1$ is odd, then $t = (s t)^{r} s (s t)^{- r}$ , so $s, t$ are conjugate in $W_{a f f} \subseteq W_{e}$ and their parameters agree (The Iwahori–Matsumoto affine Hecke algebra of a based root datum).

[F2]

For any Coxeter system with finite simple set and the stated generic unit parameters, the generic reduced products indexed by the Coxeter group form a basis after every commutative coefficient specialization, with no flatness assumption (The standard basis of the generic Hecke algebra and base change).

[F3]

As a crossed product, $H_{a f f} ⋊ Ω$ has underlying vector space $H_{a f f} \otimes_{C} C [Ω]$ , and $C [Ω]$ has the group elements $U_{ω}$ as a basis (The Iwahori–Matsumoto affine Hecke algebra of a based root datum).

[F4]

Any two reduced expressions of the same affine Weyl group element are connected by braid moves (Matsumoto's theorem: braid connectivity of reduced expressions, with singleton detection in dihedral subgroups).

Proof

Given: The data above.

1.1F1F2F4givenconstruct

The affine simple set is finite by [F1]. Specialize [F2] to $v_{s} = \sqrt{q_{s}}$ ; it gives the basis ${N_{w} : w \in W_{a f f}}$ of the normalized presentation, where $N_{w}$ is a reduced product of the $N_{s}$ . For a reduced expression $w = s_{1} \dots s_{k}$ , the unnormalized product is $T_{w} = (\prod_{j = 1}^{k} v_{s_{j}}) N_{w}$ . By [F4], changing reduced expressions uses braid moves. An even braid preserves the product of the $v_{s}$ factors because both sides have equal counts of each generator; an odd braid preserves it because its two generators are conjugate in $W_{a f f}$ and [F1] makes their parameters equal. Thus the scalar is well defined and nonzero, so the unnormalized products $T_{w}$ are nonzero scalar multiples of the basis elements $N_{w}$ . Hence ${T_{w} : w \in W_{a f f}}$ is a $C$ -basis of $H_{a f f}$ .

2.1F3step 1.1algebra∎

By [F3], every element of the crossed product has a unique finite sum $\sum_{ω \in Ω} h_{ω} U_{ω}$ with $h_{ω} \in H_{a f f}$ . Expanding each coefficient uniquely in the basis from step 1.1 gives a unique finite $C$ -linear combination of $T_{w} U_{ω}$ . Hence the displayed family is a basis. No choice principle is used.

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

Maarten Solleveld, Affine Hecke Algebras and Their Representations (standard reference, not scraped)