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 three-term Rouquier braid equivalence in type A2

Example

In type $A_{2}$ ( $n = 3$ , $s = s_{1}$ , $t = s_{2}$ ) the example writes the two $8$ -term complexes $F_{s} F_{t} F_{s}$ and $F_{t} F_{s} F_{t}$ explicitly, applies the decompositions $B_{s} B_{t} B_{s} ≅ B_{s t s} \oplus B_{s}$ and $B_{t} B_{s} B_{t} ≅ B_{s t s} \oplus B_{t}$ together with $B_{s} B_{s} ≅ B_{s} (1) \oplus B_{s} (- 1)$ and $B_{t} B_{t} ≅ B_{t} (1) \oplus B_{t} (- 1)$ , exhibits the contractible summands (with extra bimodule $B_{s}$ respectively $B_{t}$ ) and their contracting homotopies, and identifies the surviving common complex built from $B_{s t s}$ ; the explicit chain maps then realize $F_{s} F_{t} F_{s} ≃ F_{t} F_{s} F_{t}$ with no shift. All terms, the shifts of $B_{s t s}$ , and the differentials of the surviving complexes are displayed.

Facts & Assumptions

Given: The adjacent simple reflections $s = s_{1}$ , $t = s_{2}$ of $S_{3}$ , the complexes $F_{s}, F_{t}$ of The positive and negative Rouquier generator complexes, and the rank-two longest bimodule $B_{s t s} = R \otimes_{R^{S_{3}}} R (3)$ of The rank-two longest type-A Soergel bimodule.

[F1]

Rank one. $B_{s} \otimes_{R} B_{s} ≅ B_{s} (1) \oplus B_{s} (- 1)$ and $B_{t} \otimes_{R} B_{t} ≅ B_{t} (1) \oplus B_{t} (- 1)$ , split by the middle-slot idempotents attached to $R = R^{s} \oplus α_{s} R^{s}$ and $R = R^{t} \oplus α_{t} R^{t}$ ; the summands are $i m (e_{+}) ≅ B_{∙} (1)$ and $i m (e_{-}) ≅ B_{∙} (- 1)$ . (The rank-one Soergel bimodule square splits)

[F2]

Rank two. $B_{s} B_{t} B_{s} ≅ B_{s t s} \oplus B_{s}$ and $B_{t} B_{s} B_{t} ≅ B_{s t s} \oplus B_{t}$ with no additional shift. (Rank-two type-A Soergel bimodule decompositions, The rank-two longest type-A Soergel bimodule)

[F3]

Gaussian elimination. An invertible differential block $φ : U \to V$ in a fixed biproduct decomposition of two adjacent terms can be cancelled, leaving a homotopy equivalent reduction and a contractible two-term complex $[U \overset{φ}{\to} V]$ . (Gaussian elimination splits a contractible two-term complex)

[F4]

Totalization. The signed tensor totalization of three two-term complexes is concentrated in cohomological degrees $0, 1, 2, 3$ , with the terms obtained by choosing one term from each factor and the Koszul differential; a unit term contributes its factor $R (\pm 1)$ in the corresponding cohomological degree. (Bounded graded bimodule complexes and signed tensor totalization)

[F5]

The three-term relation is $F_{s} F_{t} F_{s} ≃ F_{t} F_{s} F_{t}$ with no grading shift. The specific splitting and maps used in this example will be checked locally below. (Rouquier complexes satisfy the three-term braid relation)

Verification

technique · direct

1.1F4givenalgebra

Put $S = B_{s}$ , $T = B_{t}$ , $L = B_{s t s}$ . The terms of $K = F_{s} F_{t} F_{s}$ in degrees $0, 1, 2, 3$ are $S T S$ , $U \oplus V \oplus W = (T S) (1) \oplus (S S) (1) \oplus (S T) (1)$ , $A \oplus B \oplus C = S (2) \oplus T (2) \oplus S (2)$ , and $R (3)$ . The complex $K^{'}$ has this list with $s, t$ exchanged. With $m_{s}, m_{t}$ denoting multiplication, $d_{K}^{0} = (m_{s} \otimes 1 \otimes 1, 1 \otimes m_{t} \otimes 1, 1 \otimes 1 \otimes m_{s}), d_{K}^{2} = (m_{s}, - m_{t}, m_{s}),$ and $d_{K}^{1} = (\begin{array}{ccc} - m_{t} \otimes 1 & m_{s} \otimes 1 & 0 \\ - 1 \otimes m_{s} & 0 & m_{s} \otimes 1 \\ 0 & - 1 \otimes m_{s} & 1 \otimes m_{t} \end{array}) .$ In particular every component of $d^{1} d^{0}$ cancels in pairs, and the same holds for $d^{2} d^{1}$ .

1.2F1givenalgebra

Write $x = x_{1}$ , $y = x_{2}$ , $z = x_{3}$ , $β_{s} = x - y$ , $β_{t} = y - z$ and $D_{s} (f) = (f - s (f)) / (2 β_{s})$ ; these are coordinate roots, rather than the balanced roots used for negative generators. Define $J (r \otimes r^{'}) = - r \otimes β_{t} \otimes 1 \otimes r^{'} - r \otimes 1 \otimes β_{t} \otimes r^{'}, p (r \otimes f \otimes g \otimes r^{'}) = r D_{s} (f g) \otimes r^{'} .$ The coefficient operator $D_{s}$ is $R^{s}$ -linear, so $p$ is balanced across the outer $R^{s}$ dividers and middle multiplication is $R^{t}$ -balanced. Unit insertion into $S S$ is balanced, and $β_{t} \otimes 1 + 1 \otimes β_{t}$ is central in $T$ because $R = R^{t} \oplus β_{t} R^{t}$ and $β_{t}^{2} \in R^{t}$ ; hence $J$ is a bimodule map. The shifts make both maps degree zero. The identity $s (β_{t}) = β_{t} + β_{s}$ gives $D_{s} (β_{t}) = - 1 / 2$ and $p J = 1_{S}$ .

2.1F1F2step 1.2algebra

The map $j : L \to S T S$ , $j (r \otimes r^{'}) = r \otimes 1 \otimes 1 \otimes r^{'}$ , is balanced since $R^{S_{3}}$ slides across all dividers, and $p j = 0$ . To identify its image, expand the second middle slot in the $R^{t}$ -basis ${1, z}$ and slide invariant coefficients into the first middle slot; expand that slot in the $R^{s}$ -basis ${1, x}$ and slide coefficients left. Since $z \in R^{s}$ slides right, $S T S$ is generated as a bimodule by $g_{0} = 1 \otimes 1 \otimes 1 \otimes 1$ and $g_{x} = 1 \otimes x \otimes 1 \otimes 1$ . For $e = J p$ and $u = x + y - z$ , balancing gives $(1 - e) g_{0} = g_{0}, (1 - e) g_{x} = \frac{1}{2} (u g_{0} + g_{0} u) .$ Indeed $p (g_{x}) = \frac{1}{2} (1 \otimes 1)$ and the two middle $β_{t}$ tensors sum to $u g_{0} + g_{0} u - 2 g_{x}$ . Therefore $\ker p = im (1 - e) = im j$ . By F2 and $p J = 1$ , $L$ and $\ker p$ have equal finite dimensions in every graded degree, so $j$ is an isomorphism onto $\ker p$ . Thus the specific splitting is $K^{0} = j (L) \oplus J (S)$ .

3.1F1F3step 1.1step 1.2step 2.1

Split $V = (S S) (1) = V_{+} \oplus V_{-} = S (2) \oplus S$ by F1 using the coordinate middle root $β_{s}$ , a unit multiple of the balanced root. Projection to $V_{-}$ is $r \otimes f \otimes r^{'} \mapsto r D_{s} (f) \otimes r^{'}$ , whose composite with the $V$ component of $d_{K}^{0}$ is $p$ . It is the identity on $J (S)$ and zero on $j (L)$ . Cancel the identity pair $S \to V_{-}$ by F3. The surviving $L$ components into $U, V_{+}, W$ are the outer-unit inclusions with signs $+, +, +$ .

4.1F3step 1.1step 3.1algebra

The second pivot is $V_{+} \to A = 1_{S (2)}$ , while its component into $C$ is $- 1_{S (2)}$ . Gaussian elimination deletes this pair and replaces the old $C$ row by the sum of the old $C$ and $A$ rows. In degrees $0, 1, 2, 3$ the survivor is $H : L \overset{d_{H}^{0}}{\to} (T S) (1) \oplus (S T) (1) \overset{d_{H}^{1}}{\to} S (2) \oplus T (2) \overset{d_{H}^{2}}{\to} R (3),$ with $d_{H}^{0} = (j_{t s}, j_{s t}), d_{H}^{1} = (\begin{array}{cc} - m_{t} \otimes 1 & 1 \otimes m_{t} \\ - 1 \otimes m_{s} & m_{s} \otimes 1 \end{array}), d_{H}^{2} = (m_{s}, - m_{t}),$ where $j_{t s} (r \otimes r^{'}) = r \otimes 1 \otimes r^{'}$ and likewise for $j_{s t}$ . These are the remaining $U, W$ components of the preceding differential and $C, B$ components of the following one.

5.1step 1.2step 2.1step 3.1step 4.1algebra

Apply steps 1.2–4.1 to $K^{'}$ with $s, t$ exchanged. Here $D_{t} (β_{s}) = - 1 / 2$ ; the complement calculation is transported by $x \leftrightarrow z$ , negating both coordinate roots and leaving $J p$ unchanged. Reorder its survivor $H^{'}$ into the displayed order for $H$ . Its differentials are $d_{H^{'}}^{0} = d_{H}^{0}$ , $d_{H^{'}}^{1} = - d_{H}^{1}$ , $d_{H^{'}}^{2} = - d_{H}^{2}$ , by exchanging the rows and columns of the displayed middle matrix. Thus the degreewise map $q = (1, 1, - 1, 1) : H \to H^{'}$ is a chain isomorphism. Every term and map has the same written internal shifts.

6.1F3F5step 3.1step 4.1step 5.1∎

For a pivot block $(\begin{array}{cc} a & b \\ c & 1 \end{array})$ , the Gaussian chain isomorphism $T$ has components $T^{n} = (\begin{array}{cc} 1 & 0 \\ c & 1 \end{array})$ , $T^{n + 1} = (\begin{array}{cc} 1 & - b \\ 0 & 1 \end{array})$ and identity elsewhere. Its inclusion, projection and homotopy are $ι = T^{- 1} in$ , $π = pr T$ , $h = T^{- 1} k T$ , where $k$ sends the pivot target back to its source by the identity and vanishes elsewhere. Compose the two eliminations by $i = ι_{1} ι_{2}$ , $p = π_{2} π_{1}$ , $h = h_{1} + ι_{1} h_{2} π_{1}$ , and similarly for $K^{'}$ . F3 gives $p i = 1_{H}$ and $1_{K} - i p = d h + h d$ , and the primed identities. All entries are the neighboring blocks displayed above. Thus the explicit chain maps $Φ = i^{'} q p : K \to K^{'}, Ψ = i q^{- 1} p^{'} : K^{'} \to K$ satisfy $Ψ Φ = i p$ and $Φ Ψ = i^{'} p^{'}$ , with the written contractions. This verifies the relation of F5 with no grading shift.

Depends on

Used by

Nothing in the library uses this result yet.

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

Raphaël Rouquier, Categorification of the braid groups, arXiv:math/0409593v1 (30 September 2004), §3 "The 2-braid group" (standard reference, not scraped)
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)
Nicolas Libedinsky, Gentle introduction to Soergel bimodules I: the basics, São Paulo J. Math. Sci. 13 (2019), arXiv:1702.00039v2, §4 (standard reference, not scraped)