TheoremStatement: 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.

The type-A Soergel Hom formula

Statement

Let $M, N$ be objects of the type-A Soergel category ${S B i m}_{n}$ , that is, graded direct summands of finite direct sums of shifts of Bott–Samelson bimodules $B_{i_{1}} \otimes_{R} \dots \otimes_{R} B_{i_{r}}$ (the idempotent completion of the Bott–Samelson category of The type-A Soergel category ${S B i m}_{n}$ ). Then ${Hom}_{R - R} (M, N)$ is a graded free $R$ -module of graded rank $rk {Hom}_{R - R} (M, N) = \sum_{x, d, e} (M : Δ_{x} (d)) (N : \nabla_{x} (e)) v^{d - e},$ which under the Hecke normalization $T_{x} \mapsto$ the standard basis of The type-A Hecke algebra in Soergel normalization is the standard pairing $⟨ h_{Δ} (M), h_{\nabla} (N) ⟩$ of the two characters with $⟨ {\tilde{T}}_{x}, {\tilde{T}}_{y} ⟩ = δ_{x y}$ . In particular $Hom (M, M)$ is free of the same rank, and ${End}_{R - R} (R) = R$ is generated in degree $0$ .

Facts & Assumptions

Given: Objects $M, N$ of ${S B i m}_{n}$ , graded direct summands of Bott–Samelson bimodules, and the characters $h_{Δ}, h_{\nabla}$ of Standard graph bimodules, support filtrations and characters.

[F1]

Special Hom formula: for $M^{'} \in F_{Δ}$ and $B$ a Bott–Samelson bimodule, ${Hom}_{R - R} (M^{'}, B)$ is graded free of rank $\sum (M^{'} : Δ_{x} (d)) (B : \nabla_{x} (e)) v^{d - e}$ , and dually for a Bott–Samelson source and a $\nabla$ -flagged target (Special Bott–Samelson Hom formula before reflection localization).

[F2]

Imported from Soergel's Lemma 6.13 with Satz 6.14, in the normalization recorded in the definition: for $M^{'} \in F_{Δ}$ and $N^{'} \in add B$ the graded module ${Hom}_{R - R} (M^{'}, N^{'})$ is free of rank $\sum_{x, d, e} (M^{'} : Δ_{x} (d)) (N^{'} : \nabla_{x} (e)) v^{d - e}$ , and the same expression is obtained for $M^{'} \in add B$ and $N^{'} \in F_{\nabla}$ ; moreover $add B = B$ , where $B$ consists of the bimodules $B$ for which $B \oplus C ≅ D$ with $C, D$ finite sums of shifted Bott–Samelson products; it is this category of special bimodules that is closed under direct summands (Standard graph bimodules, support filtrations and characters).

[F3]

${S B i m}_{n}$ is the idempotent completion of the category of Bott–Samelson bimodules; every object is a direct summand of a finite direct sum of shifts of Bott–Samelson bimodules and hence lies in $add B$ , with finite support, in $F_{Δ} \cap F_{\nabla}$ , and with intrinsic multiplicities, and finite freeness on both sides is inherited by summands (The type-A Soergel category ${S B i m}_{n}$ , The type-A support filtration multiplicities are intrinsic, Bott–Samelson bimodules carry delta and nabla support filtrations, Type-A top support layers are controlled by reflection localization).

[F4]

The character sums are $h_{Δ} (M) = \sum_{x, d} (M : Δ_{x} (d)) v^{d} {\tilde{T}}_{x}$ and $h_{\nabla} (N) = \sum_{x, e} (N : \nabla_{x} (e)) v^{- e} {\tilde{T}}_{x}$ with ${\tilde{T}}_{x} = v^{ℓ (x)} T_{x}$ , and $⟨ {\tilde{T}}_{x}, {\tilde{T}}_{y} ⟩ = δ_{x y}$ defines the standard pairing of the Hecke algebra, bilinear over $Z [v, v^{- 1}]$ (Standard graph bimodules, support filtrations and characters, The type-A Hecke algebra in Soergel normalization).

Proof

1.1

Reduction to the imported instance: by [F3] every object of ${S B i m}_{n}$ is a direct summand of a finite direct sum of shifts of Bott–Samelson bimodules, so it lies in the additive closure $add B$ and, by [F3] again, in $F_{Δ} \cap F_{\nabla}$ with intrinsic multiplicities; both sides of the displayed formula are additive in each variable, because the multiplicities are additive over the layers of a support flag and the graded rank is additive over direct sums. It therefore suffices to invoke the imported identity [F2] for the pair $(M, N)$ , which is the instance $M \in F_{Δ}$ , $N \in add B$ (the dual instance $M \in add B$ , $N \in F_{\nabla}$ gives the same displayed expression and the same conclusion). [F2, F3] 1.2 Freeness and rank: [F2] gives that ${Hom}_{R - R} (M, N)$ is a graded free $R$ -module of rank $\sum_{x, d, e} (M : Δ_{x} (d)) (N : \nabla_{x} (e)) v^{d - e}$ , the multiplicities being the intrinsic ones of [F3]; in particular $Hom (M, M)$ is free of the same rank with $M = N$ . [F2, F3] 1.3 Consistency with the locally proved special case: for $M$ a Bott–Samelson bimodule the same formula is [F1], and the two agree because [F3] identifies the multiplicities used in [F2] with the multiplicities of the support flags of $M$ and $N$ ; [F3]'s localization input, the rank identities of Type-A top support layers are controlled by reflection localization, exhibits the top layer of each flag as the corresponding hom space. [F1, F3] 2.1 Hecke normalization: expanding the two characters by [F4] and using the bilinearity of the standard pairing with $⟨ {\tilde{T}}_{x}, {\tilde{T}}_{y} ⟩ = δ_{x y}$ gives $⟨ h_{Δ} (M), h_{\nabla} (N) ⟩ = \sum_{x, d, e} (M : Δ_{x} (d)) (N : \nabla_{x} (e)) v^{d - e}$ , which is the displayed rank, so the graded rank is the standard pairing of the two characters. [F4, step 1.2] 3.1 Unit: for $M = N = R$ the two flags have the single quotient $Δ_{e} (0) = \nabla_{e} (0) = R$ , so the formula gives rank $v^{0} = 1$ and $h_{Δ} (R) = h_{\nabla} (R) = {\tilde{T}}_{e} = 1$ , and ${End}_{R - R} (R) = R$ is generated in degree $0$ ; the general case is [F2] together with the identification of step 2.1. ∎

F2step 1.2step 2.1

Depends on

Used by

Light leaf maps form bases of type-A Soergel homs to the unit Theorem

Dependency tree · two levels

20 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, Lemma 6.13, Satz 6.14, PDF pp.17–22 (standard reference, not scraped)
Elias–Williamson, Soergel Calculus, §3.5 (standard reference, not scraped)