ExampleConstruction: Literature-sourcedVerification: 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.

The Rouquier complex of a positive three-strand braid

Example

For the positive word $σ_{1} σ_{2} \in B_{3}$ the Rouquier complex is $F (σ_{1} σ_{2}) = [B_{1} \otimes_{R} B_{2} \overset{d^{0}}{\to} B_{1} (1) \oplus B_{2} (1) \overset{d^{1}}{\to} R (2)]$ with cohomological degrees $0, 1, 2$ and differentials $d^{0} (x \otimes y) = (x \cdot ε_{2} (y), ε_{1} (x) \cdot y), d^{1} (a \otimes r, s \otimes b) = ε_{1} (a) r - s ε_{2} (b),$ under the evident identifications $B_{1} \otimes_{R} R (1) = B_{1} (1)$ , $R (1) \otimes_{R} B_{2} = B_{2} (1)$ and $R (1) \otimes_{R} R (1) = R (2)$ ; the example checks $d^{1} d^{0} = 0$ on the four left-basis tensors $u_{1} \otimes u_{2}$ , $u_{1} \otimes (1 \otimes α_{2})$ , $(1 \otimes α_{1}) \otimes u_{2}$ , and $(1 \otimes α_{1}) \otimes (1 \otimes α_{2})$ of $B_{1} \otimes_{R} B_{2}$ , where $u_{i} = 1 \otimes 1$ and records the cohomological and internal degree of every generator.

Facts & Assumptions

Given: The adjacent simple reflections $s_{1}, s_{2}$ of $S_{3}$ , the bimodules $B_{1}, B_{2}$ with the generators $u_{i} = 1 \otimes 1$ of degree $- 1$ and $1 \otimes α_{i}$ of degree $1$ , and the complexes $F_{1} = [B_{1} \overset{ε_{1}}{\to} R (1)]$ , $F_{2} = [B_{2} \overset{ε_{2}}{\to} R (1)]$ of The positive and negative Rouquier generator complexes.

[F1]

Generators and products. $B_{i}$ has the left $R$ -basis $(1 \otimes 1, 1 \otimes α_{i})$ of degrees $- 1$ and $1$ ; the multiplication $ε_{i}$ sends $1 \otimes 1 \mapsto 1$ and $1 \otimes α_{i} \mapsto α_{i}$ , and satisfies $ε_{i} (r \otimes r^{'}) = r r^{'}$ (The positive and negative Rouquier generator complexes).

[F2]

Totalization. The signed tensor totalization of $F_{1}$ and $F_{2}$ has cohomological degree terms $F^{0} \otimes G^{0} = B_{1} \otimes_{R} B_{2}$ , $F^{0} \otimes G^{1} \oplus F^{1} \otimes G^{0} = B_{1} (1) \oplus B_{2} (1)$ and $F^{1} \otimes G^{1} = R (2)$ , with Koszul differential $d (x \otimes y) = d_{F} (x) \otimes y + (- 1)^{p} x \otimes d_{G} (y)$ for $x \in F^{p}$ (Bounded graded bimodule complexes and signed tensor totalization).

Verification

technique · direct

1.1F1F2

The degree- $0$ term is $B_{1} \otimes_{R} B_{2}$ , of cohomological degree $0$ ; the degree- $1$ term is $F^{0} \otimes G^{1} \oplus F^{1} \otimes G^{0} = B_{1} \otimes_{R} R (1) \oplus R (1) \otimes_{R} B_{2} ≅ B_{1} (1) \oplus B_{2} (1)$ ; the degree- $2$ term is $R (1) \otimes_{R} R (1) ≅ R (2)$ . The four basis monomials $u_{1} \otimes u_{2}$ , $u_{1} \otimes (1 \otimes α_{2})$ , $(1 \otimes α_{1}) \otimes u_{2}$ , $(1 \otimes α_{1}) \otimes (1 \otimes α_{2})$ of $B_{1} \otimes_{R} B_{2}$ have internal degrees $- 2, 0, 0, 2$ ; the basis $u_{i}, 1 \otimes α_{i}$ of $B_{i} (1)$ has degrees $- 2, 0$ ; and the generator of $R (2)$ has degree $- 2$ .

2.1F2step 1.1

Under the identifications of step 1.1 the Koszul differentials are $d^{0} (x \otimes y) = (x \cdot ε_{2} (y), ε_{1} (x) \cdot y) \in B_{1} (1) \oplus B_{2} (1)$ and $d^{1} (a, s) = ε_{1} (a) - ε_{2} (s)$ computed in $R (2)$ , i.e. $d^{1} (a \otimes r, s \otimes b) = ε_{1} (a) r - s ε_{2} (b)$ in the notation of the display; the minus sign is the Koszul sign on the differential from bidegree $(1, 0)$ to $(1, 1)$ , where the first factor $R (1)$ sits in cochain degree $1$ .

3.1F1step 2.1

For every simple tensor $x \otimes y \in B_{1} \otimes_{R} B_{2}$ one computes $d^{1} d^{0} (x \otimes y) = ε_{1} (x) ε_{2} (y) - ε_{1} (x) ε_{2} (y) = 0$ : the first component of $d^{0} (x \otimes y)$ contributes $ε_{1} (x) ε_{2} (y)$ and the second contributes the same product with the Koszul sign $- 1$ , so the two cancel. Since the differentials are balanced and $R$ -bilinear, this extends to all elements, so $d^{1} d^{0} = 0$ .

4.1step 1.1step 3.1∎

The degree bookkeeping of step 1.1 shows that $d^{0}$ and $d^{1}$ are homogeneous of internal degree zero on the displayed generators, hence on all elements; this records the cohomological and internal degree of every generator of the three terms and completes the verification of the displayed formula.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

Eugene Gorsky, Oscar Kivinen, José Simental, Algebra and geometry of link homology: Lecture Notes from the IHES 2021 Summer School, Bull. London Math. Soc. 55 (2023) 537-591, §3.1 (standard reference, not scraped)
Raphaël Rouquier, Categorification of the braid groups, arXiv:math/0409593v1 (30 September 2004), §3 "The 2-braid group" (standard reference, not scraped)