TheoremStatement: 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 canonical Hecke trace is symmetric and perfect

Statement

Let $(S, m)$ , $W$ , $R$ , $H$ , the standard basis ${T_{w} : w \in W}$ , and the trace $τ$ be as in Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy, The standard basis of the generic Hecke algebra and base change, and The canonical Hecke trace and symmetrizing form. Assume $W$ is finite. On the finite free $R$ -module $E = ⨁_{w \in W} R e_{w}$ , define the coordinate pairing by $⟨ e_{x}, e_{y} ⟩ = δ_{x, y}$ and extend $R$ -bilinearly. For an endomorphism $A$ with $A (e_{x}) = \sum_{y} a_{y, x} e_{y}$ , define its coordinate transpose by $A^{t} (e_{y}) = \sum_{x} a_{y, x} e_{x}$ , so $⟨ A u, v ⟩ = ⟨ u, A^{t} v ⟩$ . Let $P_{s}$ be the left length operator of The commuting left and right length operators and their Hecke relations.

For all $x, y \in W$ ,

τ (T_{x} T_{y}) = δ_{x^{- 1}, y} .

Consequently $τ (a b) = τ (b a)$ for all $a, b \in H$ , and the map $H \to {Hom}_{R} (H, R)$ , $a \mapsto [b \mapsto τ (a b)]$ , is an isomorphism. The basis dual to ${T_{w} : w \in W}$ for this pairing is ${T_{w^{- 1}} : w \in W}$ ; it is the standard basis indexed by inverses, not the algebra-inverse family ${T_{w}^{- 1}}$ .

For every unital homomorphism of commutative rings $ϕ : R \to R^{'}$ , the induced canonical trace on $R^{'} \otimes_{R} H$ has the same basis-pair formula and is again symmetric and perfect. No semisimplicity, field, or nondegeneracy hypothesis is required.

Facts & Assumptions

Given: A finite Coxeter system $(W, S)$ , its generic Hecke algebra $H$ over $R$ , its standard basis, the finite-rank regular module $E$ , and the coefficient-at-identity functional $τ$ .

[F1]

For $s \in S$ , $P_{s} (e_{w}) = e_{s w}$ if $ℓ (s w) = ℓ (w) + 1$ , and $P_{s} (e_{w}) = e_{s w} + (v_{s} - v_{s}^{- 1}) e_{w}$ if $ℓ (s w) = ℓ (w) - 1$ . (The commuting left and right length operators and their Hecke relations)

[F2]

For every reduced expression $w = s_{1} \dots s_{k}$ , $P_{s_{1}} \dots P_{s_{k}} (e_{1}) = e_{w}$ . (The commuting left and right length operators and their Hecke relations)

[F3]

The standard-basis representation $ρ : H \to {End}_{R} (E)$ satisfies $ρ (T_{w}) = P_{w}$ and $ρ (T_{w}) (e_{1}) = e_{w}$ ; the standard elements remain a basis after every commutative base change of $R$ . (The standard basis of the generic Hecke algebra and base change)

[F4]

For finite $W$ , if $h = \sum_{w \in W} r_{w} T_{w}$ , then $τ (h) = r_{1}$ . (The canonical Hecke trace and symmetrizing form)

Proof

Given: The data of the Statement.

1.1givenF1algebra

Fix $s \in S$ . The involution $w \mapsto s w$ has no fixed point because [F1] gives $ℓ (s w) = ℓ (w) \pm 1$ . It partitions $W$ into pairs; in each pair let $w_{-}$ be the unique shorter element and write the other element as $s w_{-}$ . Put $a_{s} = v_{s} - v_{s}^{- 1}$ . Then $P_{s} (e_{w_{-}}) = e_{s w_{-}}$ and $P_{s} (e_{s w_{-}}) = e_{w_{-}} + a_{s} e_{s w_{-}}$ . Relative to the ordered pair $(e_{w_{-}}, e_{s w_{-}})$ , its matrix is $(\begin{array}{cc} 0 & 1 \\ 1 & a_{s} \end{array})$ , which is symmetric. Distinct pairs are preserved, so $⟨ P_{s} u, v ⟩ = ⟨ u, P_{s} v ⟩$ for every $u, v \in E$ : each $P_{s}$ is self-adjoint for the coordinate pairing.

2.1F1F2step 1.1algebra

If $x = s_{1} \dots s_{k}$ is reduced, then its reversed word $s_{k} \dots s_{1}$ represents $x^{- 1}$ and is reduced: otherwise its inverse word would give a shorter expression for $x$ . Thus $P_{x} = P_{s_{1}} \dots P_{s_{k}}$ and, since each factor is self-adjoint, its adjoint is $P_{x}^{t} = P_{s_{k}} \dots P_{s_{1}} = P_{x^{- 1}}$ . By [F2], $P_{x^{- 1}} e_{1} = e_{x^{- 1}}$ and $P_{y} e_{1} = e_{y}$ .

3.1F2F3F4step 2.1

Write $T_{x} T_{y} = \sum_{w \in W} r_{w} T_{w}$ . Since the representation $ρ$ in [F3] is an algebra homomorphism, applying $ρ (T_{x} T_{y})$ to $e_{1}$ gives $P_{x} P_{y} e_{1} = \sum_{w} r_{w} P_{w} e_{1} = \sum_{w} r_{w} e_{w}$ . Thus [F4] and the coordinate pairing show that the coefficient of $T_{1}$ is $⟨ e_{1}, P_{x} P_{y} e_{1} ⟩$ . Move $P_{x}$ across the pairing using step 2.1 to obtain

τ (T_{x} T_{y}) = ⟨ P_{x^{- 1}} e_{1}, P_{y} e_{1} ⟩ = ⟨ e_{x^{- 1}}, e_{y} ⟩ = δ_{x^{- 1}, y} .

This proves the basis-pair formula.

4.1givenstep 3.1algebra

Since $δ_{x^{- 1}, y} = δ_{y^{- 1}, x}$ , the formula of step 3.1 is symmetric on basis pairs; $R$ -bilinearity gives $τ (a b) = τ (b a)$ for all $a, b$ . For each $z \in W$ define the coordinate functional $λ_{z} (\sum_{w} r_{w} T_{w}) : = r_{z}$ . Every $R$ -linear functional $f : H \to R$ has the unique expansion $f = \sum_{z \in W} f (T_{z}) λ_{z}$ , so ${λ_{z}}$ is a basis of ${Hom}_{R} (H, R)$ . Step 3.1 gives $[b \mapsto τ (T_{x} b)] = λ_{x^{- 1}}$ , hence the pairing map sends a basis bijectively to the dual basis and is an isomorphism. Also $τ (T_{x} T_{y^{- 1}}) = δ_{x, y}$ , proving the stated dual-basis description.

5.1F3step 3.1step 4.1∎

After any unital ring map $ϕ : R \to R^{'}$ , [F3] gives the specialized basis ${1 \otimes T_{w} : w \in W}$ . Its canonical trace has the same coefficient formula, so the calculation of step 3.1 gives the same permutation Gram matrix over $R^{'}$ . The coordinate functionals for this finite basis again form a basis of the $R^{'}$ -dual by the explicit coordinate argument of step 4.1; therefore the specialized trace is symmetric and perfect. All constructions use the already indexed basis and finite coordinate formulas, so no choice or semisimplicity is used.

Depends on

Used by

Cited to discharge well-definedness by The canonical Hecke trace and symmetrizing form.

Dependency tree · two levels

20 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

Meinolf Geck, Modular Representations of Hecke Algebras (EPFL lecture notes, arXiv:math/0511548v2) (standard reference, not scraped)
George Lusztig, Hecke Algebras with Unequal Parameters (revised book text, arXiv:math/0208154v2) (standard reference, not scraped)
Andrew Mathas, Iwahori-Hecke Algebras and Schur Algebras of the Symmetric Group (self-contained notes, 1998; complete 79-page text) (standard reference, not scraped)