TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Minimal positive Rouquier complexes carry the induced Hodge-Riemann signs

Facts & Assumptions

Given: A symmetric group $S_{n}$ , an element $x$ with a fixed reduced expression $\underline{x} = s_{1} \dots s_{m}$ of length $m = ℓ (x)$ , the minimal Rouquier complex $F_{x} \subseteq^{\oplus} F_{s_{1}} \dots F_{s_{m}}$ and its terms $^{j} F_{x}$ for $j \geq 0$ (Minimal complexes and the perverse truncations in the real type-A Soergel category, The Bott–Samelson bimodule of a word); for each $j$ the set $π (x, j)$ of subexpressions of $\underline{x}$ obtained by deleting $j$ letters and the direct sum $⨁_{x^{'} \in π (x, j)} B S (x^{'})$ with its intersection form; a tuple $λ = (λ_{x^{'}})$ of strictly positive real numbers and the rescaled form $⟨ b, b^{'} ⟩_{λ} = \sum_{x^{'}} λ_{x^{'}} ⟨ b_{x^{'}}, b_{x^{'}}^{'} ⟩_{B S (x^{'})}$ ; the operator $L_{0} = ρ \cdot (-)$ of left multiplication by a strictly dominant $ρ$ ; the hypothesis $S (\leq x)$ and the ascent Hodge-Riemann statements $H R (y, s)$ for all $y < x$ and simple $s$ with $y s > y$ (Primitive subspaces, hard Lefschetz and the Hodge-Riemann signs: the dictionary of hypotheses S, hL and HR); and the embeddings $Γ_{\geq y} F_{x} / Γ_{> y} F_{x}$ of the $Δ$ -split complex (Positive Rouquier complexes are Delta-split).

[F1]

Since $F_{x}$ is a direct summand of $F_{s_{1}} \dots F_{s_{m}}$ and $^{j} (F_{s_{1}} \dots F_{s_{m}}) = ⨁_{x^{'} \in π (x, j)} B S (x^{'}) (j)$ , the term $^{j} F_{x}$ is a direct summand of $⨁_{x^{'} \in π (x, j)} B S (x^{'}) (j)$ ; shifting by $(- j)$ gives the canonical inclusion $^{j} F_{x} (- j) \subseteq^{\oplus} ⨁_{x^{'} \in π (x, j)} B S (x^{'})$ used throughout, and $^{j} F_{x} (- j)$ is a $ρ$ -stable graded subspace with symmetric Betti numbers because [F2] expresses it as a sum of unshifted normalized self-dual indecomposables (Minimal complexes and the perverse truncations in the real type-A Soergel category, Invariant forms on an indecomposable Soergel bimodule are unique up to scalar, non-degenerate, and agree with the restricted Bott-Samelson form).

[F2]

Under $S (\leq x)$ the linearity theorem gives $^{0} F_{x} = B_{x}$ and $^{j} F_{x} = ⨁_{z < x} B_{z} (j)^{m_{z, j}}$ for $j \geq 1$ ; in particular every summand of $^{j} F_{x} (- j)$ is a normalized indecomposable $B_{z}$ with $z \leq x$ and $ℓ (z) \leq m - j$ (Minimal positive Rouquier complexes are linear under the lower Soergel induction).

[F3]

The tensoring lemma: if a self-dual $B = ⨁_{z} B_{z}^{R, m_{z}}$ with $m_{z} \neq 0 \Rightarrow S (z)$ and $H R (z, s)_{ζ}$ carries an invariant non-degenerate form making it even or odd and satisfying HR with the standard sign for $ρ$ , then $B B_{s}$ satisfies HR with the standard sign for $L_{ζ}$ and the induced form; moreover the restriction of the form of $B$ to a $B_{z}$ -summand is $(- 1)^{(d - ℓ (z)) / 2}$ times a positive multiple of the normalized form when the lowest degree of $B$ is $- d$ (Tensoring a direct sum of Hodge-Riemann bimodules with B_s preserves the signs).

[F4]

The stable-subspace lemma: an $L_{0}$ -stable graded subspace $V$ with symmetric Betti numbers of a space satisfying hL and HR inherits hL and HR with the ambient degree-by-degree signs; the standard global sign of $V$ agrees with the ambient standard sign when the lowest nonzero degrees agree, and in general the signature of the ambient Lefschetz form on the primitive subspaces of $V$ is the one induced by the ambient normalization (Signature constancy in a Lefschetz family, the L-stable subspace lemma and the weak-Lefschetz substitute, Hard Lefschetz gives the primitive decomposition, orthogonality and the signature formula).

[F5]

Degenerate shifted case: if on a graded space with a possibly degenerate form the operator $L$ satisfies $L^{i} : H^{- d - i} \to H^{- d + i}$ isomorphically for all $i \geq 0$ with $d > 0$ , then the Lefschetz form $(h, h^{'})_{L}^{- i} = ⟨ h, L^{i} h^{'} ⟩$ is identically zero (Signature constancy in a Lefschetz family, the L-stable subspace lemma and the weak-Lefschetz substitute).

Statement

Assume $S (\leq x)$ and $H R (y, s)$ for every $y < x$ and simple $s$ with $y s > y$ . Fix a reduced expression $\underline{x}$ of $x$ . Then $F_{x}$ satisfies the Hodge-Riemann bilinear relations in the following sense: there exists an embedding as a direct summand $F_{x} \subseteq^{\oplus} F_{s_{1}} \dots F_{s_{m}}$ such that for every tuple $λ = (λ_{x^{'}})_{x^{'} \in π (x, j)}$ of strictly positive real numbers and every $j \geq 0$ , the space $^{j} F_{x} (- j)$ embedded in $⨁_{x^{'} \in π (x, j)} B S (x^{'})$ carries the Hodge-Riemann bilinear relations with respect to the rescaled form $⟨ -, - ⟩_{λ}$ and the Lefschetz operator given by left multiplication by $ρ$ , with the global sign fixed so that the Lefschetz form is positive definite on the primitive subspaces in degrees congruent to $- m + j (m o d 4)$ . Here $π (x, j)$ is the set of subexpressions of $\underline{x}$ obtained by deleting $j$ letters and $^{j} F_{x} (- j) \subseteq^{\oplus} ⨁_{x^{'} \in π (x, j)} B S (x^{'})$ is the canonical summand inclusion of [F1]. The existence of such an embedding and all its sign conclusions hold for every reduced expression; no scalar comparison of the entire multiplicity-space forms from different expressions is required.

Proof

technique · induction over the Bruhat order; the last letter splits the complex as a summand of $F_yF_s$, the two pieces of the decomposition (6.4) are compared with the induction hypothesis and the tensoring lemma, and the source inherits the relations as a stable summand

1.1givenF1F4

Base of the induction. [base] For $x = e$ the complex is $F_{e} = S$ , $m = 0$ , and for $j = 0$ the space $^{0} F_{e} (0) = S$ satisfies hL and HR trivially: its lowest degree is $0$ , the primitive subspace $P^{0} = R$ carries the positive definite form $⟨ 1, 1 ⟩ > 0$ , and $0 \equiv - m + j (m o d 4)$ , so the global sign is the standard one; there are no $j \geq 1$ terms.

2.1givenstep 1.1F1F2

Induction hypothesis and the last letter. [ih] Fix $x \neq e$ and assume the statement for every $y < x$ . Write $\underline{x} = s_{1} \dots s_{m}$ , $y = s_{1} \dots s_{m - 1}$ and $s = s_{m}$ , so that $x = y s$ with $ℓ (x) = ℓ (y) + 1$ and $F_{x}$ is a summand of $F_{y} F_{s}$ ; fix an embedding $F_{y} \subseteq^{\oplus} F_{s_{1}} \dots F_{s_{m - 1}}$ witnessing the induction hypothesis and use it to embed $F_{x} \subseteq^{\oplus} F_{y} F_{s} \subset F_{s_{1}} \dots F_{s_{m}}$ . For every $j$ this gives the embedding chain of [F1], $^{j} F_{x} (- j) \subseteq^{\oplus}^{j} F_{y} B_{s} (- j) \oplus^{j - 1} F_{y} (- j + 1)$ , and the induction hypothesis applies to $^{j} F_{y} (- j)$ and to $^{j - 1} F_{y} (- j + 1)$ with the global signs indexed by $y$ ; by [F2] the $j$ -th term of $F_{x}$ is linear.

3.1step 2.1F2F3

The decomposition of the middle term and orthogonality. Under $S (\leq x)$ the comparison lemma gives a decomposition of the multiplicity space, so $^{j} F_{y} (- j) = ⨁_{z} V_{z} \otimes_{R} B_{z}$ with degree-zero multiplicity spaces $V_{z}$ ; define $B^{↑} = ⨁_{z s > z} V_{z} \otimes B_{z}$ and $B^{↓} = ⨁_{z s < z} V_{z} \otimes B_{z}$ , so that $^{j} F_{y} (- j) = B^{↑} \oplus B^{↓}$ . The decomposition is orthogonal for the induced form because $Hom (B^{↑}, D B^{↓}) = Hom (B^{↓}, D B^{↑}) = 0$ for non-isomorphic indecomposables under $S$ ; character calculations give that $B^{↑} B_{s}$ is perverse and that $B^{↓} B_{s} ≅ B^{↓} (- 1) \oplus B^{↓} (1)$ .

4.1step 3.1F2F5

The shifted descent piece does not contribute. In the decomposition $B^{↓} B_{s} ≅ B^{↓} (1) \oplus B^{↓} (- 1)$ the restriction of the Lefschetz form to $B^{↓} (1)$ is identically zero: left multiplication by $ρ$ satisfies hL on $B^{↓}$ (the induction hypothesis gives hL on $^{j} F_{y} (- j)$ , and its unshifted block projectors commute with $ρ$ , so each descent block inherits hL), so [F5] applies to the shifted piece with $d > 0$ . Moreover the projection of $^{j} F_{x} (- j)$ to $B^{↓} B_{s}$ lands entirely in $B^{↓} (1)$ : $^{j} F_{x} (- j)$ lives in perverse degree $0$ by the linearity theorem, and Hom-vanishing between perverse degrees $0$ and $- 1$ forces the projection to the $B^{↓} (- 1)$ -part to vanish. Hence the image of $^{j} F_{x} (- j)$ in $B^{↓} B_{s}$ contributes nothing to the Lefschetz form.

5.1step 4.1F2

All Lefschetz forms and a genuine split inclusion. The projection onto the surviving factors defines a degree-zero $ρ$ -equivariant map $ȷ :^{j} F_{x} (- j) \to B^{↑} B_{s} \oplus^{j - 1} F_{y} (- j + 1)$ . For every $k \geq 0$ and $b, b^{'}$ in source degree $- k$ , step 4.1 gives $⟨ b, ρ^{k} b^{'} ⟩ = ⟨ ȷ (b), ρ^{k} ȷ (b^{'}) ⟩$ , since the omitted shifted-descent factor contributes zero to that Lefschetz form. This is equality of all negative-degree Lefschetz forms, not a degree-one form identity. Applying $q$ to the original split inclusion yields a split inclusion; every map from its perverse source to $B^{↓} (1)$ vanishes after $q$ , since none of those differently shifted indecomposable classes are isomorphic. Hence $q (ȷ)$ is split injective. Lift a left inverse to a morphism $h$ of bimodules. Then $q (h ȷ) = 1$ , so reflection of isomorphisms by the radical quotient makes $h ȷ$ invertible. The map $(h ȷ)^{- 1} h$ is a genuine bimodule left inverse of $ȷ$ . Thus $ȷ$ is a split inclusion already before reduction and remains injective after reduction.

6.1step 5.1step 2.1F3

The codomain satisfies the relations with the global sign. The two orthogonal summands of the codomain are handled as follows. The summand $^{j - 1} F_{y} (- j + 1)$ satisfies HR with the global sign of the induction hypothesis for $y$ and $j - 1$ , namely positivity on primitive degrees congruent to $- ℓ (y) + (j - 1) = - m + 1 + j - 1 = - m + j (m o d 4)$ , which is the required global sign for $x, j$ . The summand $B^{↑} B_{s}$ satisfies HR by the tensoring lemma [F3]: $B^{↑}$ is a self-dual direct sum of normalized $B_{z}$ with $z s > z$ , each satisfying $H R (z, s)$ by hypothesis and hence hL and HR with the standard sign; its restricted form satisfies HR with the inherited global sign by the induction hypothesis and the stable-subspace lemma. Multiply this form by its global factor $ε \in {\pm 1}$ to give the standard sign, apply [F3], and undo that same factor on the induced tensor form. The tensor thus has the inherited global sign shifted by one, i.e. positivity on degrees congruent to $(- ℓ (y) + j) - 1 = - m + j (m o d 4)$ . Since the two summands are orthogonal and carry the same global sign, the codomain satisfies HR with the global sign fixed by $- m + j$ .

7.1step 5.1step 6.1F2F4discharge-induction: step 2.1∎

Inheritance from the negative-degree form identities. The reduced map $ȷ$ is an injective $ρ$ -equivariant graded map into the HR space of step 6.1. Its source has symmetric dimensions by [F2] and normalized self-duality, so ambient hL makes every $ρ^{k}$ on source degree $- k$ injective, hence an isomorphism onto the opposite degree. Source primitives map into ambient primitives. The identity for every $k$ in step 5.1 therefore makes each source primitive form definite with the required ambient sign. Primitive decomposition on the source now gives nonsingular Lefschetz forms in every negative degree; together with hL and graded symmetry this also proves that its original restricted invariant form is non-degenerate. Thus it satisfies HR. The embedding was chosen before the positive rescalings: the induction gives the properties for every tuple on $F_{y}$ , the orthogonal label blocks are independent of these scalars, and the split projection argument is categorical. Applying this argument for every tuple proves the full simultaneous rescaling assertion and closes the induction.

Remarks

The sign normalization "positive in degrees congruent to $- m + j$ modulo $4$ " is the one of Elias-Williamson Proposition 6.13; it is the standard sign relative to the generic lowest degree $- (m - j)$ of $^{j} F_{x} (- j)$ and is fixed once for all $j$ so that the orthogonal pieces in step 6.1 carry the same normalization.
Step 4.1 is exactly the place where the degenerate shifted case is used; the zero-parameter hard-Lefschetz theorem later separates the kernel of $d_{3}$ for the same reason, and no step of this proof asserts HR for an unseparated shifted descent target.

Depends on

Used by

Dependency tree · two levels

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