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.

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

Statement

Let $n \geq 2$ over $k = Q$ , let $\underline{x} = (x_{1}, \dots, x_{r})$ be a word in simple reflections with Bott–Samelson bimodule $B_{\underline{x}} = B_{x_{1}} \otimes_{R} \dots \otimes_{R} B_{x_{r}}$ , and let $F : D \to {B S B i m}^{∙}$ be the graded monoidal functor of The type-A diagrammatic relations hold for Soergel bimodules carrying the word $\underline{x}$ to $B_{\underline{x}}$ and the empty word to $R$ . Fix once and for all a choice of light leaves ${L L}_{\underline{x}, e} \in {Hom}_{D} (\underline{x}, \emptyset)$ as in The type-A diagrammatic Soergel category and its candidate bimodule functor, one for each subexpression $e$ of $\underline{x}$ expressing the identity element $e \in S_{n}$ , and write again ${L L}_{\underline{x}, e}$ for the evaluated bimodule map $F ({L L}_{\underline{x}, e}) : B_{\underline{x}} \to R$ . Then the evaluated light leaves ending at the identity form a homogeneous free left $R$ -basis of the graded $R$ -module ${Hom}_{R - R} (B_{\underline{x}}, R)$ : the leaf indexed by $e$ is homogeneous of degree $d (e) = # U_{0} - # D_{0}$ , the graded rank of ${Hom}_{R - R} (B_{\underline{x}}, R)$ is $\sum_{e : w_{e} = e} v^{d (e)}$ , the sum over the subexpressions of $\underline{x}$ expressing the identity, and every $R$ -linear combination of the leaves is therefore the unique one representing a given map. In particular $F$ induces a surjection ${Hom}_{D} (\underline{x}, \emptyset) \to {Hom}_{R - R} (B_{\underline{x}}, R)$ on hom spaces to the unit.

Facts & Assumptions

Given: A word $\underline{x} = (x_{1}, \dots, x_{r})$ in simple reflections, its Bott–Samelson bimodule $B_{\underline{x}}$ , the diagrammatic category $D$ with its light leaves, and the functor $F : D \to {B S B i m}^{∙}$ of The type-A diagrammatic relations hold for Soergel bimodules.

[F1]

$F$ respects every defining relation of $D$ , hence descends to a graded $Q$ -linear monoidal functor $D \to {B S B i m}^{∙}$ with $\underline{x} \mapsto B_{\underline{x}}$ and $\emptyset \mapsto R$ ; a diagram of degree $d$ is carried to a bimodule map of degree $d$ . After finite sums and shifts and restriction to degree-zero maps, it extends by idempotent completion to $Kar (D) \to {S B i m}_{n}$ (The type-A diagrammatic relations hold for Soergel bimodules, The type-A diagrammatic Soergel category and its candidate bimodule functor).

[F2]

Light leaves: for every word $\underline{x}$ , every $w \in S_{n}$ and every subexpression $e$ of $\underline{x}$ expressing $w$ after fixing a reduced word $\underline{w}$ for $w$ , there is a light leaf ${L L}_{\underline{x}, e} : \underline{x} \to \underline{w}$ in $D$ of degree $d (e) = # U_{0} - # D_{0}$ ; for $\underline{y} = \emptyset$ the only admissible product is $w = e$ , and the light leaves ${L L}_{\underline{x}, e}$ with $e$ expressing the identity form a homogeneous free $R$ -basis of ${Hom}_{D} (\underline{x}, \emptyset)$ (The type-A diagrammatic Soergel category and its candidate bimodule functor, Double leaves form graded $R$ -bases of type-A diagrammatic Hom spaces).

[F3]

Imported defect expansion (Elias–Williamson, §2.4, Lemma 2.10 with Corollary 2.11, in the normalization $H_{s} = v T_{s} + v$ ): for a word $\underline{x} = (x_{1}, \dots, x_{m})$ one has $\sum_{e} v^{d (e)} {\tilde{T}}_{w_{e}} = H_{x_{1}} \dots H_{x_{m}}$ , and equivalently the $Δ$ -multiplicity of the standard bimodule $Δ_{w} (d)$ in $B_{\underline{x}}$ is the number of subexpressions of $\underline{x}$ expressing $w$ with defect $d$ , $(B_{\underline{x}} : Δ_{w} (d)) = # {e : w_{e} = w, d (e) = d}$ (The type-A diagrammatic Soergel category and its candidate bimodule functor).

[F4]

Soergel's Hom formula: for objects $M, N$ of ${S B i m}_{n}$ , ${Hom}_{R - R} (M, N)$ is graded free of graded rank $\sum_{x, d, e} (M : Δ_{x} (d)) (N : \nabla_{x} (e)) v^{d - e}$ (The type-A Soergel Hom formula).

[F5]

The trivial bimodule is $Δ_{e} (0) = \nabla_{e} (0) = R$ , generated in degree $0$ , and $Δ_{e} (d) = \nabla_{e} (d) = R (d)$ in general; a standard bimodule $R_{x}$ with $x \neq e$ has $\nabla$ -multiplicity concentrated on the single graph $G r (x)$ (Standard graph bimodules, support filtrations and characters).

[F6]

Imported localised independence (Elias–Williamson, §6.7, Remark 6.29 with the localisation argument of the proof of Corollary 6.8): with the light leaves chosen once and for all, each $F ({L L}_{\underline{x}, e})$ is a composition of the images of dots, trivalent vertices and $2 m_{s t}$ -valent vertices, and the images of the light leaves ${L L}_{\underline{x}, e}$ for $e$ expressing a fixed $w$ are linearly independent over $R$ in $Hom (B_{\underline{x}}, B_{\underline{w}})$ (The type-A diagrammatic Soergel category and its candidate bimodule functor).

Proof

1.1

The evaluated leaves are well defined and homogeneous: by [F1] the functor $F$ is defined on $D$ and preserves degrees in total graded Hom, and by [F2] each ${L L}_{\underline{x}, e}$ with $e$ expressing the identity is a morphism $\underline{x} \to \emptyset$ in $D$ of degree $d (e)$ ; its image is therefore an element of ${Hom}_{R - R} (B_{\underline{x}}, R)$ homogeneous of degree $d (e)$ , and the family is indexed by the finite set of subexpressions of $\underline{x}$ expressing the identity together with their target choice.

F1F2

1.2

Linear independence: by [F6], the images of the light leaves ${L L}_{\underline{x}, e}$ with $e$ expressing the identity are linearly independent over $R$ inside $Hom (B_{\underline{x}}, R)$ ; since $R$ is a domain this is the same as independence over the fraction field of $R$ .

2.1

Rank of the target: by [F4] applied to $M = B_{\underline{x}}$ and $N = R = \nabla_{e} (0)$ , and by [F5], only the terms with $x = e$ and $e = 0$ survive, so that ${Hom}_{R - R} (B_{\underline{x}}, R)$ is graded free of graded rank $\sum_{d} (B_{\underline{x}} : Δ_{e} (d)) v^{d}$ ; by [F3] this multiplicity is the number of subexpressions of $\underline{x}$ expressing the identity with defect $d$ , so the rank is $\sum_{e : w_{e} = e} v^{d (e)}$ , the same finite sum of monomials as in step 1.1.

F3F4F5

3.1

Dimension count: let $V$ be the free graded $R$ -module with a homogeneous basis element $b_{e}$ of degree $d (e)$ , one for each subexpression $e$ of $\underline{x}$ expressing the identity; the $R$ -linear map $V \to {Hom}_{R - R} (B_{\underline{x}}, R)$ , $b_{e} \mapsto {L L}_{\underline{x}, e}$ , is degree preserving and injective by step 1.2. By step 2.1 the target is graded free with the same graded rank as $V$ , hence in every degree $k$ the source and target of the $k$ -th degree piece are $Q$ -vector spaces of the same finite dimension, and the injective degree- $k$ map is an isomorphism; therefore the evaluated light leaves span as well as being independent, and they are a basis.

step 2.1step 1.2

4.1

Conclusion: the evaluated light leaves ending at the identity form a homogeneous free left $R$ -basis of ${Hom}_{R - R} (B_{\underline{x}}, R)$ , their degrees are the defects $d (e)$ , and the graded rank is $\sum_{e : w_{e} = e} v^{d (e)}$ ; in particular $F$ is surjective on ${Hom}_{D} (\underline{x}, \emptyset) \to {Hom}_{R - R} (B_{\underline{x}}, R)$ , because the images of the diagrammatic basis already span the target. For $\underline{x} = \emptyset$ the family has the single member $e = \emptyset$ of defect $0$ , and ${Hom}_{R - R} (R, R) = R$ is the free $R$ -module of rank $v^{0}$ generated by the identity, so the statement specialises to the unit. ∎

F2step 3.1

Remark

(a) Which input is imported and which is checked here. The content of Libedinsky's Théorème 5.1 (Elias–Williamson, §7, Proposition 7.6 in the diagrammatic formulation) is recorded as imported results 8 and 1 of The type-A diagrammatic Soergel category and its candidate bimodule functor; the linear independence of the evaluated leaves is recorded there as imported result 11 and is not reproved here. What this item does is to identify the graded rank of the target with the total defect count using the library's Hom formula of The type-A Soergel Hom formula and the defect expansion of imported result 10, and to deduce the basis statement from independence and that rank.

(b) Basis here, span there. The same argument without step 2.1 gives only that the evaluated leaves are independent; the degree comparison is what upgrades independence to a basis, exactly as in the source's Remark 6.29. The span statement for the whole hom space between Bott–Samelson bimodules is the next item, obtained from this one by Frobenius biadjunction.

(c) Choice. No choice principle is used. The finitely many light leaves have to be chosen once and for all, as the sources note; the subexpressions of a word are finite, $R$ is a domain, and the dimension count is performed degree by degree on finitely generated free modules.

Depends on

Used by

Evaluated double leaves form bases of type-A Soergel bimodule homs Theorem

Dependency tree · two levels

24 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

Libedinsky, Sur la catégorie des bimodules de Soergel, §§3–5 (standard reference, not scraped)
Elias–Williamson, Soergel Calculus, §6.1 Construction 6.1, §6.2 Proposition 6.12, §6.7 Remark 6.29, PDF pp. 57–63, 69 (standard reference, not scraped)