LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

Special Bott–Samelson Hom formula before reflection localization

Statement

Suppose either that $M \in F_{Δ}$ is a graded $R$ -bimodule with a $Δ$ -flag and $N$ is a Bott–Samelson bimodule $B_{\underline{i}} = B_{i_{1}} \otimes_{R} \dots \otimes_{R} B_{i_{r}}$ (or a finite direct sum of shifts of such), or that $M$ is such a Bott–Samelson bimodule and $N \in F_{\nabla}$ . In either case ${Hom}_{R - R} (M, N)$ is a graded free $R$ -module of graded rank $rk {Hom}_{R - R} (M, N) = \sum_{x \in S_{n}} \sum_{d, e \in Z} (M : Δ_{x} (d)) (N : \nabla_{x} (e)) v^{d - e},$ with the multiplicities and characters of Standard graph bimodules, support filtrations and characters, which by The type-A support filtration multiplicities are intrinsic depend only on $M$ and $N$ . This is Soergel's Theorem 5.15 restricted to Bott–Samelson targets and sources; it precedes the reflection-localization statement for arbitrary direct summands.

Facts & Assumptions

Given: A graded $R$ -bimodule $M$ with a $Δ$ -flag (or a Bott–Samelson bimodule), a Bott–Samelson bimodule $N$ , simple reflections $s$ , and the characters $h_{Δ}, h_{\nabla}$ of Standard graph bimodules, support filtrations and characters.

[F1]

${Hom}_{R - R} (B_{s} \otimes_{R} M, N) ≅ {Hom}_{R - R} (M, B_{s} \otimes_{R} N)$ and ${Hom}_{R - R} (M \otimes_{R} B_{s}, N) ≅ {Hom}_{R - R} (M, N \otimes_{R} B_{s})$ as graded $R$ -modules, naturally in $M, N$ (Frobenius biadjunction for the type-A Soergel generators).

[F2]

Separately on the two flag categories, Soergel Propositions 5.7(2) and 5.9(2) give $h_{Δ} (B_{s} \otimes_{R} M) = H_{s} h_{Δ} (M)$ for $M \in F_{Δ}$ and $h_{\nabla} (B_{s} \otimes_{R} N) = H_{s} h_{\nabla} (N)$ for $N \in F_{\nabla}$ , with $H_{s} = {\tilde{T}}_{s} + v$ . These follow by summing the two respective multiplicity recursions in Remark (d)(1) of Standard graph bimodules, support filtrations and characters against $v^{d} {\tilde{T}}_{x}$ and $v^{- d} {\tilde{T}}_{x}$ . The Hecke identity is $H_{s} {\tilde{T}}_{y} = {\tilde{T}}_{s y} + v {\tilde{T}}_{y}$ for $s y > y$ and ${\tilde{T}}_{s y} + v^{- 1} {\tilde{T}}_{y}$ for $s y < y$ , using The standard basis of the type-A Hecke algebra and its multiplication rule. Shifting a layer reindexes $d$ and gives $h_{Δ} (M {k}) = v^{- k} h_{Δ} (M)$ and $h_{\nabla} (N {k}) = v^{k} h_{\nabla} (N)$ on their respective domains. Intrinsicness on each category separately follows from the corresponding canonical layers in Remark (d)(7) of the same definition; no simultaneous pair of flags is required.

[F3]

The multiplicity pairing $⟨, ⟩$ on the Hecke algebra with $⟨ {\tilde{T}}_{x}, {\tilde{T}}_{y} ⟩ = δ_{x y}$ is symmetric and $H_{s}$ is self-adjoint for it: $⟨ H_{s} F, G ⟩ = ⟨ F, H_{s} G ⟩$ , because the standard pairing is the coefficient of ${\tilde{T}}_{e}$ in $i (F) G$ for the anti-involution $i (v) = v$ , $i ({\tilde{T}}_{x}) = {\tilde{T}}_{x^{- 1}}$ , and $i (H_{s}) = H_{s}$ (Soergel, proof of Theorem 5.15) (The standard basis of the type-A Hecke algebra and its multiplication rule).

[F4]

${Hom}_{R - R} (R_{v} (a), R_{w} (b)) ≅ R (b - a)$ for $v = w$ and $0$ for $v \neq w$ , where $R (b - a)$ denotes the free module generated in degree $a - b$ (Standard graph bimodules, support filtrations and characters).

[F5]

Bott–Samelson bimodules lie in $F_{Δ} \cap F_{\nabla}$ and the functors $B_{s} \otimes_{R} -$ and $- \otimes_{R} B_{s}$ preserve both flag categories and preserve finite freeness (Bott–Samelson bimodules carry delta and nabla support filtrations).

[F6]

The imported Hom formula of Soergel Theorem 5.15, recorded as result 6 in Standard graph bimodules, support filtrations and characters, gives the base case $N = R = B_{\emptyset}$ : for every $M \in F_{Δ}$ , ${Hom}_{R - R} (M, R)$ is graded free of rank $\sum_{d} (M : Δ_{e} (d)) v^{d}$ . Its proof supplies the exactness over a $Δ$ -flag needed for this base case. The same imported result separately gives the dual case of a Bott–Samelson source and $N \in F_{\nabla}$ . The library rank convention sends a generator of degree $a$ to $v^{a}$ and is the $v \mapsto v^{- 1}$ transform of Soergel Notation 5.2.

Proof

1.1

Reduction step: by [F1] the two hom spaces $Hom (B_{s} \otimes_{R} M, N)$ and $Hom (M, B_{s} \otimes_{R} N)$ are isomorphic as graded $R$ -modules, hence have the same graded rank; by [F2] the right hand sides of the claimed formula for the two pairs differ by the factor $H_{s}$ on the two sides and agree by the self-adjointness of [F3], so the formula holds for the pair $(B_{s} \otimes_{R} M, N)$ if and only if it holds for $(M, B_{s} \otimes_{R} N)$ .

F1F2F3

1.2

Shift step: the same argument with $M$ replaced by $M {k}$ uses $Hom (M {k}, N) ≅ Hom (M, N {- k})$ and the shift rules of [F2] to show that the formula for $(M {k}, N)$ is equivalent to the formula for $(M, N {- k})$ .

1.3

Base case: let $N = R = B_{\emptyset}$ . The first imported case of [F6] applies to $M \in F_{Δ}$ and this Bott–Samelson target, so ${Hom}_{R - R} (M, R)$ is graded free with rank $\sum_{x, d, e} (M : Δ_{x} (d)) (R : \nabla_{x} (e)) v^{d - e}$ . The one-graph flag of $R$ has $(R : \nabla_{e} (0)) = 1$ and no other quotients, so this reduces to $\sum_{d} (M : Δ_{e} (d)) v^{d}$ . The single-layer calculation $Hom (Δ_{e} (d), R) ≅ R (- d)$ of [F4] agrees with that grading; the passage from a flag to the full Hom module uses the imported exactness in [F6], not the single-layer vanishing alone.

F4F6

1.4

Induction on the word: write a nonempty Bott–Samelson target as $N = B_{s} \otimes_{R} N^{'}$ by peeling its leftmost letter. The first biadjunction of [F1] gives $Hom (M, B_{s} \otimes_{R} N^{'}) ≅ Hom (B_{s} \otimes_{R} M, N^{'})$ . By [F5], $B_{s} \otimes_{R} M \in F_{Δ}$ , so the induction hypothesis computes the rank of the latter Hom module as $⟨ h_{Δ} (B_{s} \otimes_{R} M), h_{\nabla} (N^{'}) ⟩$ . The left recursion of [F2] and self-adjointness in [F3] turn this into $⟨ H_{s} h_{Δ} (M), h_{\nabla} (N^{'}) ⟩ = ⟨ h_{Δ} (M), H_{s} h_{\nabla} (N^{'}) ⟩ = ⟨ h_{Δ} (M), h_{\nabla} (B_{s} \otimes_{R} N^{'}) ⟩$ , the claimed rank for $(M, N)$ .

F1F2F3F5

1.5

Dual case: when $M$ is Bott–Samelson and $N \in F_{\nabla}$ , the imported dual assertion [F6] gives freeness and the displayed rank directly. Taking opposites does not exchange the two flag categories, so it is not used for this step.

2.1

Conclusion: finite direct sums of shifts of words are handled by additivity of Hom and of the canonical support layers, with the shift rule of step 1.2. Thus for every pair $(M, N)$ covered by the statement the graded rank of ${Hom}_{R - R} (M, N)$ is the displayed multiplicity sum, and by the first-case induction together with [F6] the hom space is a free graded $R$ -module; the shift and simple-reflection moves of steps 1.1 to 1.5 generate every Bott–Samelson word, so no further hypothesis on $N$ is used and the reflection-localization statement for arbitrary direct summands is not invoked. ∎

step 1.1step 1.2step 1.3step 1.4step 1.5

Depends on

Used by

Dependency tree · two levels

17 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

Soergel, Kazhdan–Lusztig-Polynome und unzerlegbare Bimoduln, Theorem 5.15 and its proof, PDF p.17 (standard reference, not scraped)
Elias–Williamson, Soergel Calculus, §3.5 (standard reference, not scraped)