ExampleConstruction: Literature-sourcedVerification: 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 rank-one Soergel bimodule: trace form, reduced module and hard Lefschetz

Example

Take $n = 2$ , so $S_{n} = {e, s}$ and $B_{s} = B_{s}^{R} = S \otimes_{S^{s}} S (1)$ with $S = R [x_{1}, x_{2}]$ , $\deg x_{i} = 2$ and $α_{s} = x_{1} - x_{2}$ . In the right $S$ -basis ${c_{i d}, c_{s}}$ of degrees $- 1$ and $+ 1$ the multiplication relations are $c_{i d} c_{i d} = c_{i d}, c_{i d} c_{s} = c_{s}, c_{s} c_{s} = c_{s} α_{s} .$ The trace is $Tr (c_{i d} a + c_{s} b) = b$ for $a, b \in S$ and the intersection form has the Gram matrix $(\begin{array}{cc} ⟨ c_{i d}, c_{i d} ⟩ & ⟨ c_{i d}, c_{s} ⟩ \\ ⟨ c_{s}, c_{i d} ⟩ & ⟨ c_{s}, c_{s} ⟩ \end{array}) = (\begin{array}{cc} 0 & 1 \\ 1 & α_{s} \end{array}),$ whose determinant is $- 1$ , so the form is non-degenerate, and the induced form on the reduced module is non-degenerate too. The reduced module has the real basis $(\overline{c_{i d}}, \overline{c_{s}})$ with degrees $- 1$ and $+ 1$ , so $\dim (\overline{B_{s}})^{- 1} = \dim (\overline{B_{s}})^{1} = 1$ ; for $ρ = α_{s} / 2 = (x_{1} - x_{2}) / 2$ , which is strictly dominant with $ρ (α_{s}^{\lor}) = 1$ , one computes $ρ \cdot \overline{c_{i d}} = \overline{c_{s}}$ and $ρ \cdot \overline{c_{s}} = 0$ . Hence $ρ : (\overline{B_{s}})^{- 1} \to (\overline{B_{s}})^{1}$ is an isomorphism, hard Lefschetz holds, the primitive subspace in degree $- 1$ is all of $(\overline{B_{s}})^{- 1}$ , and the Lefschetz form $(a, b) = ⟨ a, ρ b ⟩$ is positive on it: $⟨ \overline{c_{i d}}, \overline{c_{s}} ⟩ = 1 > 0$ , matching the Hodge-Riemann sign $(- 1)^{(ℓ (s) - 1) / 2} = + 1$ . Finally $ch (B_{s}) = H_{s} + v = {\underline{H}}_{s}$ , the Kazhdan-Lusztig basis element of the simple reflection, which is Soergel's conjecture at $s$ , and the rational model over $Q$ gives the same numbers.

Verification

technique · direct computation in the right basis of the rank-one bimodule

Given: The rank-one data above: $B_{s} = S \otimes_{S^{s}} S (1)$ with right basis $c_{i d} = 1 \otimes 1$ (degree $- 1$ ) and $c_{s} = \frac{1}{2} (α_{s} \otimes 1 + 1 \otimes α_{s})$ (degree $+ 1$ ), the trace and intersection form of the Bott-Samelson bimodule (The trace, the invariant intersection form on Bott-Samelson bimodules and its reduction, The Soergel bimodule $B_{i}$ of a simple reflection), the reduced module and dominant operator (The reduced Soergel module and the dominant Lefschetz operator, The real type-A Soergel category by scalar extension), and the HR dictionary (Primitive subspaces, hard Lefschetz and the Hodge-Riemann signs: the dictionary of hypotheses S, hL and HR).

[F1] The left action satisfies $r \cdot c_{i d} = c_{i d} \cdot s (r) + \partial_{s} (r) c_{s}$ and $r \cdot c_{s} = c_{s} \cdot r$ ; the products are $c_{i d} c_{i d} = c_{i d}$ , $c_{i d} c_{s} = c_{s}$ , $c_{s} c_{s} = c_{s} α_{s}$ ; the trace is the coefficient of $c_{s}$ in the right basis, and $⟨ b, b^{'} ⟩ = Tr (b b^{'})$ (The trace, the invariant intersection form on Bott-Samelson bimodules and its reduction).

[F2] The reduction $\overline{M} = M / M S_{+}$ kills right multiples by positive-degree elements; a non-degenerate invariant form descends to a non-degenerate form on the reduction, and the induced form on the reduced module is the one used in the HR dictionary (The reduced Soergel module and the dominant Lefschetz operator, The trace, the invariant intersection form on Bott-Samelson bimodules and its reduction).

[F3] For a graded space with lowest degree $- d$ hard Lefschetz requires $ρ^{i} : ()^{- i} \to ()^{i}$ to be isomorphisms, the primitive subspaces are $P^{- i} = \ker (ρ^{i + 1})$ and the standard sign in degree $- i$ is $(- 1)^{(d - i) / 2}$ (Primitive subspaces, hard Lefschetz and the Hodge-Riemann signs: the dictionary of hypotheses S, hL and HR, Hard Lefschetz gives the primitive decomposition, orthogonality and the signature formula).

[F4] The standard character sums the $Δ_{y} (d)$ layers with coefficients $v^{d} H_{y}$ , where $Δ_{y} (d) = S_{y} (d - ℓ (y))$ (Standard graph bimodules, support filtrations and characters). The bar-fixed triangular element at a simple reflection is $H_{s} + v = {\underline{H}}_{s}$ (Existence and uniqueness of the Kazhdan–Lusztig basis).

1.1givenF1

Products and the trace. The multiplication rules are those of [F1]. By definition the trace extracts the coefficient of $c_{s}$ in the right basis, so $Tr (c_{i d} a + c_{s} b) = b$ for $a, b \in S$ .

2.1step 1.1F1F2

The Gram matrix and non-degeneracy. Using $⟨ b, b^{'} ⟩ = Tr (b b^{'})$ and the products of step 1.1, $⟨ c_{i d}, c_{i d} ⟩ = Tr (c_{i d}) = 0$ , $⟨ c_{i d}, c_{s} ⟩ = Tr (c_{s}) = 1$ and $⟨ c_{s}, c_{s} ⟩ = Tr (c_{s} α_{s}) = α_{s}$ , so the Gram matrix in the basis $(c_{i d}, c_{s})$ is $(\begin{array}{cc} 0 & 1 \\ 1 & α_{s} \end{array})$ ; its determinant is $- 1$ , hence the form is non-degenerate, and by [F2] so is the induced form on the reduced module.

2.2step 1.1F1F2

The reduced action of $ρ$ . Let $ρ = α_{s} / 2$ . Since $ρ$ is $s$ -anti-invariant, $s (ρ) = - ρ$ and $\partial_{s} (ρ) = 1$ , so by [F1] we get $ρ \cdot c_{i d} = c_{i d} \cdot (- ρ) + c_{s} = c_{s} - c_{i d} ρ$ ; reducing kills the right multiple $c_{i d} ρ$ by [F2], so $ρ \cdot \overline{c_{i d}} = \overline{c_{s}}$ . Similarly $ρ \cdot c_{s} = c_{s} ρ$ by [F1] and $c_{s} ρ$ is a right multiple by a positive-degree element, so $ρ \cdot \overline{c_{s}} = 0$ . Also $ρ (α_{s}^{\lor}) = 1 > 0$ , so $ρ$ is strictly dominant.

3.1step 2.1step 2.2F3

Hard Lefschetz, primitivity and the sign. The reduced module has real basis $\overline{c_{i d}}$ in degree $- 1$ and $\overline{c_{s}}$ in degree $+ 1$ , hence both graded pieces are one-dimensional; by step 2.2 the degree-one Lefschetz map $ρ : (\overline{B_{s}})^{- 1} \to (\overline{B_{s}})^{1}$ sends a basis vector to a basis vector and is an isomorphism, which is hard Lefschetz by [F3]. The primitive subspace is $P^{- 1} = \ker (ρ^{2} ∣_{(\overline{B_{s}})^{- 1}}) = (\overline{B_{s}})^{- 1}$ , since $ρ^{2}$ maps the one-dimensional space to the higher space in two steps and $ρ^{2}$ lands in degree $+ 3$ , which is zero; the Lefschetz form on it is $⟨ \overline{c_{i d}}, ρ \overline{c_{i d}} ⟩ = ⟨ \overline{c_{i d}}, \overline{c_{s}} ⟩ = 1 > 0$ , the reduction of the Gram entry $1$ , and the standard sign in degree $- 1$ is $(- 1)^{(1 - 1) / 2} = + 1$ , so HR holds with the standard sign and the bottom form is positive.

4.1step 3.1F1F2F4∎

The character. Multiplication $B_{s} \to S (1)$ is surjective with kernel generated on the right by $k = c_{s} - c_{i d} α_{s}$ , of degree $1$ . The left-action rule gives $r k = k s (r)$ , so the kernel is $S_{s} (- 1) = Δ_{s} (0)$ and the quotient is $S (1) = Δ_{e} (1)$ . These two layers give $ch (B_{s}) = H_{s} + v = {\underline{H}}_{s}$ . The top graph layer has generator degree $+ 1$ and the unit quotient has generator degree $- 1$ . The rational model has the same formulas after real scalar extension.

Remarks

This is the base case of the rank-one computations used both in the counterexample on the non-dominant element and in the base of the simultaneous induction; the two-dimensional reduced module has a one-dimensional primitive space in degree $- 1$ , and the sign $+ 1$ is the standard sign.
The trace normalization is the one of the Bott-Samelson intersection form; no freedom remains after the normalizations of the page, since the form is unique up to scalar and the trace fixes the scalar by $Tr (c_{s}) = 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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