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 finite type-A Hecke basis over the multiplicative parameter ring

Statement

Let $n \geq 2$ , $R_{0} = Z [Q, Q^{- 1}]$ , and let $H_{n, Q}^{f i n}$ be the unital associative $R_{0}$ -algebra presented by generators $T_{1}, \dots, T_{n - 1}$ , relations $(T_{i} - Q) (T_{i} + 1) = 0$ , and the type- $A_{n - 1}$ braid relations. For $w \in S_{n}$ , let $T_{w}$ be the product along a reduced expression of $w$ . Then $T_{w}$ is well-defined and

{T_{w} : w \in S_{n}}

is an $R_{0}$ -basis of $H_{n, Q}^{f i n}$ . For every commutative $R_{0}$ -algebra $R^{'}$ , the scalar extension $R^{'} \otimes_{R_{0}} H_{n, Q}^{f i n}$ has basis $(1 \otimes T_{w})_{w \in S_{n}}$ .

Facts & Assumptions

Given: The type- $A_{n - 1}$ Coxeter group $S_{n}$ , the ring $R_{0} = Z [Q, Q^{- 1}]$ , and the finite Hecke presentation in the Statement.

[F1]

Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification: the type- $A_{n - 1}$ Coxeter group on adjacent transpositions identifies with $S_{n}$ .

[F2]

Matsumoto's theorem: braid connectivity of reduced expressions, with singleton detection in dihedral subgroups: any two reduced expressions of one Coxeter-group element are related by a finite sequence of braid moves.

[F3]

The standard basis of the generic Hecke algebra and base change: over the one-parameter Laurent ring $Z [v, v^{- 1}]$ , the finite generic Hecke algebra with generators $U_{i}$ and relations $(U_{i} - v) (U_{i} + v^{- 1}) = 0$ has basis $(U_{w})_{w \in S_{n}}$ and that basis survives commutative base change.

[F4]

The reversal anti-involution, generator invertibility, the bar operator and the multiplicative normalization: for the same parameter on all type-A generators, $T_{i} = v U_{i}$ and $Q = v^{2}$ convert $(U_{i} - v) (U_{i} + v^{- 1}) = 0$ into $(T_{i} - Q) (T_{i} + 1) = 0$ ; scaling every braid word of a fixed length multiplies both sides by the same power of $v$ .

[F5]

Multivariate polynomial and Laurent rings over commutative rings, domains and fraction fields: Laurent polynomial rings are free on their Laurent monomials; in particular the powers $v^{k}$ form a $Z$ -basis of $Z [v, v^{- 1}]$ .

[F6]

Presentation base change and transport of explicit bases to commutative specializations: scalar extension of a presented algebra is the algebra presented by the images of its relations, and scalar extension of a free module carries its basis to the tensor images, with no flatness assumption.

[F7]

The free associative R-algebra on a set and descent of relations: quotienting the free associative algebra by the finite Hecke and braid relations defines the unital associative algebra with that presentation.

Proof

Given: The data of the Statement.

1.1F1F2F7algebra

The free associative presentation and its quotient exist by [F7]. If two reduced expressions of $w$ are chosen, [F2] connects them by braid moves; each move is one defining braid relation in $H_{n, Q}^{f i n}$ . The corresponding products therefore agree, defining $T_{w}$ independently of the chosen reduced expression.

1.2F3F4F5F6algebra

Let $R_{v} : = Z [v, v^{- 1}]$ and define $φ : R_{0} \to R_{v}$ by $φ (Q) = v^{2}$ . By [F5], each Laurent polynomial in $v$ has a unique even-power part plus $v$ times a unique even-power part, so $R_{v} = R_{0} \oplus v R_{0}$ as an $R_{0}$ -module; in particular $φ$ is injective. By [F6], $R_{v} \otimes_{R_{0}} H_{n, Q}^{f i n}$ is presented by the same braid relations and scalar-extended quadratic relations. The assignments $1 \otimes T_{i} \mapsto v U_{i}$ give an $R_{v}$ -algebra homomorphism to the generic finite Hecke algebra of [F3], since $(v U_{i} - v^{2}) (v U_{i} + 1) = v^{2} (U_{i} - v) (U_{i} + v^{- 1}) = 0$ ; scaling both sides of each braid relation by $v$ to its number of factors preserves that relation. The inverse assignment is $U_{i} \mapsto v^{- 1} (1 \otimes T_{i})$ : its quadratic relation is $v^{- 2} (T_{i} - Q) (T_{i} + 1) = 0$ , and the same equal-length argument preserves braids. The two maps are inverse on generators and coefficients, so this is an isomorphism.

2.1F3F5step 1.2algebra

Under this isomorphism, $1 \otimes T_{w}$ maps to $v^{ℓ (w)} U_{w}$ for any reduced expression of $w$ . By [F3], $(U_{w})_{w \in S_{n}}$ is an $R_{v}$ -basis, and each $v^{ℓ (w)}$ is a unit; hence $(1 \otimes T_{w})_{w \in S_{n}}$ is a basis after extension to $R_{v}$ . Let $M : = ⨁_{w \in S_{n}} R_{0} e_{w}$ and $ψ : M \to H_{n, Q}^{f i n}$ send $e_{w}$ to $T_{w}$ . Relative to $R_{v} = R_{0} \oplus v R_{0}$ , the map $R_{v} \otimes_{R_{0}} ψ$ is $ψ \oplus ψ$ . Since this map is an isomorphism by the preceding basis calculation, $ψ$ is both injective and surjective: injectivity follows from injectivity of $ψ \oplus ψ$ , and for any $h$ the element $(h, 0)$ has a preimage $(m_{1}, m_{2})$ , giving $ψ (m_{1}) = h$ . Thus $(T_{w})$ is the asserted $R_{0}$ -basis.

3.1F6step 2.1

For a commutative $R_{0}$ -algebra $R^{'}$ , [F6] identifies $R^{'} \otimes_{R_{0}} H_{n, Q}^{f i n}$ with the presentation obtained by applying $R_{0} \to R^{'}$ to the defining relations and carries the free basis of step 2.1 to $(1 \otimes T_{w})_{w \in S_{n}}$ . No property of $R^{'}$ beyond being a commutative $R_{0}$ -algebra is needed.

4.1F1F2F3F4F5F6step 1.1step 1.2step 2.1step 3.1∎

The preceding steps prove the well-defined reduced products, the universal basis, and its arbitrary commutative base change. All coefficient extensions and the rank-two free decomposition are explicit; no Choice principle is used.

Depends on

Used by

Dependency tree · two levels

66 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 lecture notes, arXiv:math/0108172 (standard reference, not scraped)
Anders Björner and Francesco Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), complete author-hosted book (standard reference, not scraped)
I. G. Macdonald, Affine Hecke algebras and orthogonal polynomials, Séminaire Bourbaki 797, Astérisque 237 (1996), pp. 189–207 (standard reference, not scraped)