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.

Embedding theorem: local intersection forms are isometric to primitive Lefschetz forms

Facts & Assumptions

Given: $x, s$ with $x s > x$ and the assumption $S (y)$ and $H R (y)$ for all $y < x s$ ; fixed reduced-word embeddings and the induced non-degenerate invariant forms on $B_{y}^{R}$ and $M : = B_{x}^{R} B_{s}^{R}$ ; a reduced expression $\underline{x}$ of $x$ and a generator $c_{b o t}$ of the one-dimensional space ${\overline{B_{y}^{R}}}^{- ℓ (y)}$ ; the local intersection form on $E_{y} = {Hom}^{0} (B_{y}^{R}, M)$ (The local intersection form on Hom(B_y, B_x B_s)).

[F1]

The top support layer of $B_{y}^{R}$ is the single standard module $Δ_{y} = R_{y} (- ℓ (y))$ , the quotient $Q = B_{y}^{R} / Γ_{\geq y} B_{y}^{R}$ has a $Δ$ -flag whose characters are those of the lower layers, and the graded multiplicities of the $Δ$ -flags are intrinsic; the graded rank of $Hom (N, M)$ for a $Δ$ -filtered $N$ is $⟨ h_{Δ} (N), h_{\nabla} (M) ⟩$ , additive in the $Δ$ -character (Type-A top support layers are controlled by reflection localization, The type-A Soergel Hom formula, The trace, the invariant intersection form on Bott-Samelson bimodules and its reduction).

[F2]

Under $S (y)$ the character of $B_{y}^{R}$ is ${\underline{H}}_{y}$ , so $h_{Δ} (Q) = {\underline{H}}_{y} - H_{y}$ in the standard-basis expansion, a sum with nonnegative coefficients all divisible by $v$ ; the graded rank of $Hom (Q, M)$ therefore has all its $v$ -powers positive. The restriction map $Hom (B_{y}^{R}, M) \to Hom (Δ_{y}, M)$ is the first map of the left-exact $Hom$ sequence of $0 \to Δ_{y} \to B_{y}^{R} \to Q \to 0$ . [F1]

[F3]

The generator of $Δ_{y} = R_{y} (- ℓ (y))$ has degree $+ ℓ (y)$ , so ${Hom}^{0} (Δ_{y}, M) ≅ (Γ_{y} M)^{ℓ (y)}$ . The proved right splitting of $Γ_{y} M \subseteq M$ makes its reduction inject into $\overline{M}$ . Under the present $S (< x s)$ , the Hom formula and the polynomial character $ch (M) = {\underline{H}}_{x} {\underline{H}}_{s}$ imply that ${Hom}^{∙} (B_{y}, M)$ has no negative degrees. Restriction as in step 1.1 then gives the same vanishing for ${Hom}^{∙} (Δ_{y}, M)$ ; hence $Γ_{y} M$ has no degree below $ℓ (y)$ , and its degree- $ℓ (y)$ part injects into its reduction. The normalized $B_{y}$ has one-dimensional reduced extremal degrees $\pm ℓ (y)$ , and its top $Δ_{y}$ generator reduces to a nonzero generator of degree $+ ℓ (y)$ (Type-A top support layers are controlled by reflection localization, Normalized type-A Soergel bimodules are self-dual and have length degree bounds, Indecomposable labels, characters and filtration ranks agree after real scalar extension).

[F4]

HR $(y)$ gives hL $(y)$ and the normalized bottom Lefschetz value $N : = ⟨ ρ^{ℓ (y)} c_{b o t}, c_{b o t} ⟩_{B_{y}} > 0$ , and the adjoint of a degree-zero map with respect to the non-degenerate invariant forms exists and is a degree-zero bimodule map (The local intersection form on Hom(B_y, B_x B_s), Invariant forms on an indecomposable Soergel bimodule are unique up to scalar, non-degenerate, and agree with the restricted Bott-Samelson form).

[F5]

The detection theorem: under $S (< x s)$ , non-degeneracy of all local intersection forms $(f, g)_{y}^{x, s}$ , $y < x s$ , implies $S (x s)$ (Non-degeneracy of the local intersection forms detects Soergel's conjecture one step higher).

Statement

Fix $x, s$ with $x s > x$ and assume $S (y)$ and $H R (y)$ for all $y < x s$ ; fix embeddings and the induced forms, a reduced expression $\underline{x}$ of $x$ and a generator $c_{b o t}$ of the one-dimensional space ${\overline{B_{y}^{R}}}^{- ℓ (y)}$ . Then:

the evaluation map $e v : {Hom}^{0} (B_{y}^{R}, M) \to {\overline{M}}^{- ℓ (y)}$ , $f \mapsto \overline{f} (c_{b o t})$ , where $M = B_{x}^{R} B_{s}^{R}$ and $\overline{f}$ is the induced map on right reductions, is injective with image contained in the primitive subspace $P_{ρ}^{- ℓ (y)} = \ker (ρ^{ℓ (y) + 1})$ ;
$e v$ is an isometry up to the positive factor $N = ⟨ ρ^{ℓ (y)} c_{b o t}, c_{b o t} ⟩_{\overline{B_{y}^{R}}} > 0$ : $N (f, g)_{y}^{x, s} = (e v (f), e v (g))_{ρ}^{- ℓ (y)}$ for all $f, g$ ;
consequently $H R (x, s)$ implies $S (x s)$ : a definite form restricted to a subspace stays non-degenerate, so the local forms are non-degenerate and the detection theorem applies.

Proof

technique · direct; the exact sequence of the top support layer, degreewise Hilbert-series comparison and adjointness. Evaluating a bimodule map at a reduced vector means evaluating its induced map on right reductions; the primitive spaces and real-valued Lefschetz forms below all belong to those reductions

1.1givenF1F2

The exact sequence and the degree-zero isomorphism. The top support layer gives a short exact sequence $0 \to Δ_{y} \to B_{y}^{R} \to Q \to 0$ of $Δ$ -filtered modules, and $Hom (-, M)$ is left exact, so $0 \to Hom (Q, M) \to Hom (B_{y}^{R}, M) \to Hom (Δ_{y}, M)$ is exact. By [F1] the three graded Hom spaces are free over $S$ and their graded ranks are additive in the $Δ$ -characters: $rk Hom (B_{y}^{R}, M) = rk Hom (Q, M) + rk Hom (Δ_{y}, M)$ as polynomials. By [F2] all $v$ -powers of $rk Hom (Q, M)$ are positive, so the degree- $\leq 0$ part of the map $Hom (B_{y}^{R}, M) \to Hom (Δ_{y}, M)$ is injective; comparing Hilbert series degree by degree, the two free modules have equal dimension in each degree $\leq 0$ after restriction, and the injective degreewise map is therefore an isomorphism ${Hom}^{\leq 0} (B_{y}^{R}, M) \to {Hom}^{\leq 0} (Δ_{y}, M)$ . In particular restriction of degree-zero Hom is an isomorphism, and no full graded isomorphism is asserted.

2.1step 1.1F1F3F4

Evaluation at the top and then at the bottom. Let $c \in B_{y}$ be the image of the homogeneous generator of $Δ_{y} \subseteq B_{y}$ . Its reduction spans ${\overline{B_{y}}}^{ℓ (y)}$ : the top-layer right splitting and image equality of [F3] make its reduction nonzero. By step 1.1 restriction is an isomorphism in degree zero, so evaluation at $c$ identifies the Hom space with $(Γ_{y} M)^{ℓ (y)}$ , which injects into ${\overline{M}}^{ℓ (y)}$ by [F3]. Thus $f \mapsto \overline{f (c)}$ is injective. Hard Lefschetz on $B_{y}$ , part of $H R (y)$ , says that $ρ^{ℓ (y)} c_{b o t}$ is a nonzero scalar multiple of $\overline{c}$ in that one-dimensional top degree. Therefore $ρ^{ℓ (y)} f (c_{b o t})$ is the same nonzero scalar multiple of $\overline{f (c)}$ . If bottom evaluation vanished then top evaluation would vanish, forcing $f = 0$ . Finally the degree bound ${\overline{B_{y}}}^{ℓ (y) + 2} = 0$ gives $ρ^{ℓ (y) + 1} c_{b o t} = 0$ ; bimodule linearity makes the image primitive. This proves (1), without asserting that the multiplicity space $(Γ_{y} M)^{ℓ (y)}$ is one dimensional.

3.1step 2.1F4

The isometry. For $f, g \in {Hom}^{0} (B_{y}^{R}, M)$ , the local form is $(f, g)_{y}^{x, s} = g^{*} \circ f$ , a scalar endomorphism of $B_{y}^{R}$ ; by the normalization of [F4], $N (f, g)_{y}^{x, s} = ⟨ g^{*} (f (c_{b o t})), ρ^{ℓ (y)} c_{b o t} ⟩_{B_{y}}$ , and adjointness of $g^{*}$ gives $⟨ f (c_{b o t}), ρ^{ℓ (y)} g (c_{b o t}) ⟩_{M} = (e v (f), e v (g))_{ρ}^{- ℓ (y)}$ , by definition of the Lefschetz form. The factor $N$ is positive by [F4]. This proves (2).

4.1step 3.1F5∎

From HR to the character (3). Assume HR $(x, s)$ . Since the operator $L_{0}$ on $\overline{M}$ has $P_{ρ}^{- ℓ (y)}$ as a primitive subspace and HR makes the Lefschetz form on it definite, the restriction of this form to the image $e v (E_{y})$ is non-degenerate; by the isometry of step 3.1 with the positive factor $N$ , the local intersection form on $E_{y}$ is non-degenerate. This holds for every $y < x s$ , so the detection theorem [F5], whose hypothesis $S (< x s)$ is available, gives $S (x s)$ . This proves (3) and completes the lemma.

Remarks

The degree-zero restriction isomorphism in step 1.1 is genuine only in degrees $\leq 0$ ; the full graded map $Hom (B_{y}^{R}, M) \to Hom (Δ_{y}, M)$ is not an isomorphism, which is why the proof uses graded Hilbert-series comparison rather than an ungraded rank equality.
The positivity of $N$ is part of the normalization of HR $(y)$ and enters the isometry as a positive factor, so no sign is lost when transferring definiteness between the local forms and the primitive Lefschetz forms.

Depends on

Used by

Simultaneous induction: Soergel's conjecture, hard Lefschetz and the Hodge-Riemann relations hold for all elements Theorem

Dependency tree · two levels

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