LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 Hecke trace form, its values on the Kazhdan-Lusztig basis, and the standard pairing

Facts & Assumptions

Given: The normalized type-A Hecke algebra $H = H_{v} (n)$ over $A = Z [v^{\pm 1}]$ with its standard basis $H_{w}$ , the reversal anti-involution $a$ with $a (v) = v$ and $a (H_{w}) = H_{w^{- 1}}$ , the linear functional $ε$ with $ε (H_{w}) = δ_{e, w}$ , and the bilinear form $(h, h^{'}) : = ε (a (h) h^{'})$ .

[F1]

$H$ is presented by generators $H_{s_{1}}, \dots, H_{s_{n - 1}}$ with the quadratic relations $H_{s_{i}}^{2} = 1 + (v^{- 1} - v) H_{s_{i}}$ , the adjacent braid relations and the distant commutations; the elements $H_{w}$ indexed by reduced expressions form an $A$ -basis, and right multiplication by a generator satisfies $H_{w} H_{s} = H_{w s}$ if $ℓ (w s) = ℓ (w) + 1$ , while $H_{w} H_{s} = H_{w s} + (v^{- 1} - v) H_{w}$ if $ℓ (w s) = ℓ (w) - 1$ (The normalized type-A Hecke algebra and its bar involution).

[F2]

There is an $A$ -linear involutive anti-automorphism $a$ with $a (H_{s_{i}}) = H_{s_{i}}$ and $a (H_{w}) = H_{w^{- 1}}$ for all $w$ ; in particular $a (H_{s}) = H_{s}$ for every simple reflection $s$ (Reversal anti-involution commutes with the Hecke bar).

[F3]

The Kazhdan-Lusztig elements ${\underline{H}}_{w}$ exist and are characterized by bar-invariance and ${\underline{H}}_{w} \in H_{w} + \sum_{y < w} v Z [v] H_{y}$ ; they form an $A$ -basis, and writing ${\underline{H}}_{w} = \sum_{y \leq w} p_{y, w} H_{y}$ one has $p_{w, w} = 1$ , $p_{y, w} = 0$ unless $y \leq w$ , $p_{y, w} \in v Z [v]$ for $y < w$ , and $p_{y, w} \in v^{ℓ (w) - ℓ (y)} Z [v^{- 2}]$ (The type-A Kazhdan–Lusztig basis has elementary triangular bar properties, The $R$ -coefficient recursion, support, degree bounds and inversion).

[F4]

The classical normalization is $P_{y, w} (v^{- 2}) = v^{- (ℓ (w) - ℓ (y))} p_{y, w}$ and $μ (y, w) = [v] p_{y, w}$ , and the standard basis is the normalized basis $H_{x} = v^{ℓ (x)} T_{x}$ of the Hecke page (Kazhdan–Lusztig polynomials in the classical $q$ -normalization).

Statement

Let $H = H_{v} (n)$ be the normalized type-A Hecke algebra over $A = Z [v^{\pm 1}]$ and let $a$ be the $A$ -linear anti-involution with $a (v) = v$ , $a (H_{x}) = H_{x^{- 1}}$ (the reversal anti-involution of the Hecke page). Define the trace $ε : H \to A$ by $ε (H_{w}) = δ_{e, w}$ on the standard basis, and the bilinear form $(-, -) : H \times H \to A$ by $(h, h^{'}) : = ε (a (h) h^{'})$ . Then:

$ε$ and $(-, -)$ are well defined (the $H_{w}$ are an $A$ -basis);
$(p h, q h^{'}) = p q (h, h^{'})$ for all $p, q \in A$ and all $h, h^{'}$ ;
$(h H_{s}, h^{'}) = (h, h^{'} H_{s})$ and $(H_{s} h, h^{'}) = (h, H_{s} h^{'})$ for all $h, h^{'}$ and every simple reflection $s$ ;
the standard basis is orthonormal, $(H_{x}, H_{y}) = δ_{x y}$ ;
on the Kazhdan-Lusztig basis, $({\underline{H}}_{x}, {\underline{H}}_{y}) \in v Z [v]$ for $x \neq y$ and $({\underline{H}}_{x}, {\underline{H}}_{x}) \in 1 + v Z [v]$ ;
the form of (4) is the standard pairing $⟨ H_{x}, H_{y} ⟩ = δ_{x y}$ used in the type-A Soergel Hom formula, transported through the identification of the normalized standard bases.

All statements are integral and use no choice.

Proof

technique · induction on the length in the standard basis; the ambient algebra is finite free over $A$

1.1givenF1F2

Well-definedness and bilinearity (1), (2). Since ${H_{w}}$ is an $A$ -basis by [F1], prescribing $ε (H_{w}) = δ_{e, w}$ and extending $A$ -linearly is well defined and unique; the reversal map $a$ is a well-defined $A$ -linear anti-automorphism by [F2], and multiplication is $A$ -bilinear, so $(h, h^{'}) = ε (a (h) h^{'})$ is a well-defined $A$ -bilinear form, for $(p h, q h^{'}) = ε (p a (h) q h^{'}) = p q ε (a (h) h^{'})$ with $p, q \in A$ . This proves (1) and (2).

2.1basestep 1.1F1F2

The key identity: base case and recursion. We prove by induction on $ℓ (u)$ that $ε (H_{u} H_{y}) = δ_{u, y^{- 1}}$ for all $u, y \in S_{n}$ ; for $u = e$ this reads $H_{e} H_{y} = H_{y}$ and $ε (H_{y}) = δ_{e, y} = δ_{u, y^{- 1}}$ , and for $u \neq e$ we choose a simple reflection $s$ with $ℓ (u s) = ℓ (u) - 1$ and note that [F1] applied to $w = u s$ gives $H_{u s} H_{s} = H_{u}$ , since $(u s) s = u$ has length $ℓ (u) = ℓ (u s) + 1$ .

3.1step 2.1F1F2

The left multiplication rule. Applying the anti-automorphism $a$ of [F2] to the two cases of [F1] and using $a (H_{w} H_{s}) = a (H_{s}) a (H_{w}) = H_{s} H_{w^{- 1}}$ and $(w s)^{- 1} = s w^{- 1}$ gives $H_{s} H_{w} = H_{s w}$ if $ℓ (s w) = ℓ (w) + 1$ , and $H_{s} H_{w} = H_{s w} + (v^{- 1} - v) H_{w}$ if $ℓ (s w) < ℓ (w)$ ; this is the rule used in the two cases below.

4.1step 3.1ih

The ascent case. Keep $u \neq e$ and its right descent $s$ from step 2.1, and let $y \in S_{n}$ satisfy $ℓ (s y) > ℓ (y)$ . Then $H_{s} H_{y} = H_{s y}$ by step 3.1, so $ε (H_{u} H_{y}) = ε (H_{u s} H_{s} H_{y}) = ε (H_{u s} H_{s y})$ ; the induction hypothesis applies to the pair $(u s, s y)$ , whose first length is $ℓ (u) - 1$ , giving $ε (H_{u s} H_{s y}) = δ_{u s, (s y)^{- 1}} = δ_{u s, y^{- 1} s}$ , and $u s = y^{- 1} s$ holds if and only if $u = y^{- 1}$ (multiply on the right by $s$ and use $s^{2} = e$ ), so $ε (H_{u} H_{y}) = δ_{u, y^{- 1}}$ .

5.1step 4.1ih

The descent case. Keep $u, s$ as above and let $ℓ (s y) < ℓ (y)$ . Then $H_{s} H_{y} = H_{s y} + (v^{- 1} - v) H_{y}$ by step 3.1, so $ε (H_{u} H_{y}) = ε (H_{u s} H_{s y}) + (v^{- 1} - v) ε (H_{u s} H_{y})$ ; the induction hypothesis gives $ε (H_{u s} H_{s y}) = δ_{u s, y^{- 1} s}$ and $ε (H_{u s} H_{y}) = δ_{u s, y^{- 1}}$ . If $u s = y^{- 1}$ , then $y = (u s)^{- 1} = s u^{- 1}$ and, since $u s$ is a right descent of $u$ , taking inverses gives $ℓ (y) = ℓ (s u^{- 1}) = ℓ (u s) = ℓ (u) - 1$ , while $ℓ (s y) = ℓ (u^{- 1}) = ℓ (u) > ℓ (y)$ , contradicting $ℓ (s y) < ℓ (y)$ ; hence $δ_{u s, y^{- 1}} = 0$ and $ε (H_{u} H_{y}) = δ_{u s, y^{- 1} s} = δ_{u, y^{- 1}}$ .

6.1step 2.1step 4.1step 5.1

The induction concludes. For every $u \neq e$ the cases $ℓ (s y) > ℓ (y)$ and $ℓ (s y) < ℓ (y)$ exhaust all $y$ for the chosen right descent $s$ , and each case reduced the first argument's length; with the base case this proves $ε (H_{u} H_{y}) = δ_{u, y^{- 1}}$ for all $u, y \in S_{n}$ .

7.1step 6.1F2

Standard orthonormality (4). For all $x, y$ , using $a (H_{x}) = H_{x^{- 1}}$ from [F2] and step 6.1 with $u = x^{- 1}$ , we get $(H_{x}, H_{y}) = ε (a (H_{x}) H_{y}) = ε (H_{x^{- 1}} H_{y}) = δ_{x^{- 1}, y^{- 1}} = δ_{x, y}$ , the last equality being injectivity of $w \mapsto w^{- 1}$ ; this proves (4).

7.2step 6.1F1algebra

The generator trace identity. By step 6.1, for every $w$ and simple reflection $s$ one has $ε (H_{w} H_{s}) = δ_{w, s^{- 1}} = δ_{w, s}$ and $ε (H_{s} H_{w}) = δ_{s, w^{- 1}} = δ_{w, s}$ . Extending over the standard basis gives $ε (z H_{s}) = ε (H_{s} z)$ for every $z \in H$ . In particular the common value for $w = s$ is $1$ .

8.1step 7.2F2algebra

$ε$ is a trace and yields the adjunctions (3). Every element of $H$ is a finite $A$ -linear combination of words in the generators, and moving each letter of a word for the second factor to the front one at a time with step 7.2 and bilinearity shows $ε (x y) = ε (y x)$ for all $x, y \in H$ ; consequently, for simple $s$ and $h, h^{'} \in H$ , using $a (H_{s}) = H_{s}$ from [F2], $(h H_{s}, h^{'}) = ε (a (h H_{s}) h^{'}) = ε (H_{s} a (h) h^{'}) = ε (a (h) h^{'} H_{s}) = (h, h^{'} H_{s})$ and $(H_{s} h, h^{'}) = ε (a (h) a (H_{s}) h^{'}) = ε (a (h) H_{s} h^{'}) = (h, H_{s} h^{'})$ , which proves (3) and shows both left and right multiplication by $H_{s}$ are self-adjoint for $(-, -)$ .

8.2step 7.1F3algebra

Values on the Kazhdan-Lusztig basis (5). Write ${\underline{H}}_{x} = \sum_{u \leq x} h_{u, x} H_{u}$ with $h_{u, x} = p_{u, x} \in Z [v]$ , $h_{x, x} = 1$ and $h_{u, x} \in v Z [v]$ for $u < x$ , all other coefficients zero, as in [F3]; then bilinearity (2) and orthonormality from step 7.1 give $({\underline{H}}_{x}, {\underline{H}}_{y}) = \sum_{u} h_{u, x} h_{u, y}$ . A nonzero term requires $u \leq x$ and $u \leq y$ ; if $x \neq y$ , every surviving term has a factor in $v Z [v]$ , because $u < x$ or $u < y$ is [F3], and $u = x \neq y$ gives $h_{x, y} \in v Z [v]$ when $x < y$ and $h_{x, y} = 0$ otherwise, symmetrically for $u = y$ ; hence $({\underline{H}}_{x}, {\underline{H}}_{y}) \in v Z [v]$ for $x \neq y$ . For $x = y$ the term $u = x$ contributes $h_{x, x}^{2} = 1$ and every other term has $u < x$ and contributes to $v^{2} Z [v]$ , so $({\underline{H}}_{x}, {\underline{H}}_{x}) \in 1 + v Z [v]$ .

9.1step 8.1step 8.2F3F4discharge-induction: step 5.1∎

The standard pairing (6) and conclusion. By (4) the form $(-, -)$ is the $A$ -bilinear form whose matrix in the normalized standard basis ${H_{x}}$ is the identity; the published type-A Soergel Hom formula uses the standard pairing with $⟨ H_{x}, H_{y} ⟩ = δ_{x y}$ on that normalized basis, and the dictionary of [F4] fixes the normalization $H_{x} = v^{ℓ (x)} T_{x}$ and the resulting Kazhdan-Lusztig coefficients, so the transported pairing agrees with $(-, -)$ on the basis and hence on $H$ by bilinearity. All six clauses are proved over $A = Z [v^{\pm 1}]$ , using only existence and triangularity of the Kazhdan-Lusztig basis and no positivity and no choice.

Remarks

The form is $A$ -bilinear in both arguments and not sesquilinear: the value $({\underline{H}}_{x}, {\underline{H}}_{y}) = \sum_{u} h_{u, x} h_{u, y}$ carries no coefficient conjugation. This is the form used by the type-A Soergel Hom formula.
Steps 2.1-6.1 are the local rendering of the "straightforward induction" in Elias-Williamson Section 3.2; the multiplication rules of [F1] and [F2] are the only structural inputs, and no positivity of Kazhdan-Lusztig polynomials is assumed or proved here.

Depends on

Used by

Dependency tree · two levels

12 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

Elias-Williamson, The Hodge theory of Soergel bimodules (arXiv:1212.0791v2, final version; Ann. of Math. 180 (2014) 1089-1136) (standard reference, not scraped)
Soergel, Kazhdan-Lusztig-Polynome und unzerlegbare Bimoduln ueber Polynomringen (arXiv:math/0403496, published J. Inst. Math. Jussieu 6 (2007) 501-525) (standard reference, not scraped)
Riche, La theorie de Hodge des bimodules de Soergel (d'apres Soergel et Elias-Williamson), Seminaire Bourbaki no. 1139 (arXiv:1711.02464, Octobre 2017) (standard reference, not scraped)