LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Opposite Rouquier generator complexes are homotopy inverse

Statement

$F_{i} \otimes_{R} F_{i}^{- 1} ≃ R ≃ F_{i}^{- 1} \otimes_{R} F_{i}$ in $K^{b} (R^{e} -grmod)$ , where $R$ denotes the unit complex concentrated in cohomological degree $0$ with zero differential. Explicitly, the signed tensor totalization of $F_{i}$ and $F_{i}^{- 1}$ has terms $B_{i} (- 1) ⟶ B_{i} \otimes_{R} B_{i} \oplus R ⟶ B_{i} (1)$ in cohomological degrees $- 1, 0, 1$ ; the rank-one splitting $B_{i} \otimes_{R} B_{i} ≅ B_{i} (1) \oplus B_{i} (- 1)$ exhibits two successive invertible differential blocks. Gaussian elimination splits off two contractible two-term complexes, leaving $R$ in degree $0$ . The same argument with the factors exchanged gives $F_{i}^{- 1} \otimes_{R} F_{i} ≃ R$ . All scalars occurring in the contractions are units $ε_{i}^{\pm 1}, 2^{\pm 1} \in Q$ , so the homotopy classes do not depend on the signs of the chosen normalization.

Facts & Assumptions

Given: A simple reflection $s_{i}$ , the bimodule $B_{i} = R \otimes_{R^{s_{i}}} R (1)$ with the generators $u = 1 \otimes 1$ of degree $- 1$ and $w_{0} = 1 \otimes (α_{i} / 2)$ of degree $1$ , the generator complexes $F_{i} = [B_{i} \overset{ε_{i}}{\to} R (1)]$ , $F_{i}^{- 1} = [R (- 1) \overset{η_{i}}{\to} B_{i}]$ of The positive and negative Rouquier generator complexes.

[F1]

The rank-one splitting. The invariant decomposition $R = R^{s_{i}} \oplus α_{i} R^{s_{i}}$ in the middle tensor factor gives a degree-zero bimodule isomorphism $B_{i} \otimes_{R} B_{i} ≅ B_{i} (1) \oplus B_{i} (- 1) .$ The first summand is represented by $r \otimes 1 \otimes r^{'}$ and the second by $r \otimes α_{i} \otimes r^{'}$ . This is the middle-invariant and middle- $α_{i}$ decomposition of The rank-one Soergel bimodule square splits. The outer factors form $R \otimes_{R^{s_{i}}} R$ ; in particular the outer actions of $α_{i}$ need not be equal.

[F2]

The totalization. The signed tensor totalization $K = F_{i} \otimes_{R} F_{i}^{- 1}$ has terms $K^{- 1} = B_{i} (- 1)$ , $K^{0} = B_{i} \otimes_{R} B_{i} \oplus R$ , $K^{1} = B_{i} (1)$ and Koszul differential $d (x \otimes y) = d_{F} (x) \otimes y + (- 1)^{p} x \otimes d_{G} (y)$ ; in particular $d^{- 1} (x) = ε_{i} (x) + x \otimes η_{i} (1)$ for $x \in B_{i} (- 1)$ and $d^{0}$ is $ε_{i}$ on the first tensor factor of $B_{i} \otimes_{R} B_{i}$ and $- η_{i}$ on the $R$ -summand (Bounded graded bimodule complexes and signed tensor totalization, The positive and negative Rouquier generator complexes).

[F3]

Gaussian elimination. If a cochain differential has an invertible block $φ : U \to V$ with respect to fixed biproduct decompositions $X^{n} = A \oplus U$ , $X^{n + 1} = B \oplus V$ , then $X ≃ \overset{ˉ}{X}$ for the reduction $\overset{ˉ}{X}$ obtained by deleting $U, V$ and replacing $d^{n}$ by its Schur complement, and $X ≅ \overset{ˉ}{X} \oplus K$ with $K = [U \overset{φ}{\to} V]$ a contractible two-term complex (Gaussian elimination splits a contractible two-term complex, An invertible cochain differential block and its candidate reduction).

[F4]

Contractibility. A two-term complex $[X \overset{φ}{\to} Y]$ with $φ$ invertible is contractible, and homotopy equivalent complexes have the same homotopy class; $≃$ is transitive (Complexes, homotopies and contractibility in an additive category).

Proof

technique · direct

1.1F2

The terms of $K$ are as in [F2]: over degree $- 1$ only $B_{i} \otimes R (- 1) ≅ B_{i} (- 1)$ contributes, over degree $0$ the two summands $B_{i} \otimes B_{i}$ and $R (1) \otimes R (- 1) ≅ R$ , and over degree $1$ only $R (1) \otimes B_{i} ≅ B_{i} (1)$ .

1.2F1F2algebra

Write $E = R \otimes_{R^{s_{i}}} R \otimes_{R^{s_{i}}} R$ , suppressing the common internal shifts, and denote the three copies of $α_{i}$ by $a, b, c$ . Let $S = R \otimes_{R^{s_{i}}} R$ refer to the outer factors. Since $b^{2} = c^{2}$ and every invariant balances, $E = S \oplus S b$ as an outer bimodule. The map $1 \otimes η_{i}$ sends a source element $x$ to $x (b + c)$ . Because $(b - c) (b + c) = 0$ , its value is also $x (a, c) (b + c)$ : this is immediate on the right $R^{s_{i}}$ -basis $1, α_{i}$ of the source and hence for every $x$ . Its projection to the $S b$ summand is therefore the identity $S \to S b$ under the shifted identification [F1]. This is the invertible block $B_{i} (- 1) \to B_{i} (- 1)$ of $d^{- 1}$ . No equality between the outer $a$ and $c$ is used.

2.1F2F3step 1.2

Apply Gaussian elimination [F3] to that block. It removes the degree $- 1$ term and the middle- $α_{i}$ summand, leaving a complex with $B_{i} (1) \oplus R$ in degree $0$ and $B_{i} (1)$ in degree $1$ . Its degree-zero differential is the restriction of the original $d^{0}$ to the surviving summands: the preceding cancellation changes only the coordinates associated with the eliminated block, and $d^{0} d^{- 1} = 0$ ensures that its eliminated column is zero in the new coordinates.

3.1F1F2F3F4step 2.1

On the middle-invariant summand, $ε_{i} \otimes 1$ sends $r \otimes 1 \otimes r^{'}$ to $r \otimes r^{'}$ . Hence the block $B_{i} (1) \to B_{i} (1)$ of the remaining differential is the identity. A second application of [F3] cancels it and leaves only $R$ in degree $0$ . Both canceled two-term complexes are contractible by [F4], so $F_{i} \otimes_{R} F_{i}^{- 1} ≃ R$ .

4.1F1F2F4step 3.1algebra∎

Taking the opposite bimodule interchanges left and right actions and reverses the order of a tensor product. On complexes, the identification $(X \otimes_{R} Y)^{o p} ≅ Y^{o p} \otimes_{R} X^{o p}$ sends a term of cohomological bidegree $(p, q)$ with the sign $(- 1)^{p q}$ ; direct substitution in the signed tensor differential verifies that it is a chain isomorphism. Reversing the two factors of $B_{i}$ preserves multiplication and the symmetric element $α_{i} \otimes 1 + 1 \otimes α_{i}$ , so $F_{i}^{o p} ≅ F_{i}$ and $(F_{i}^{- 1})^{o p} ≅ F_{i}^{- 1}$ . Applying this additive operation to the equivalence just proved gives $F_{i}^{- 1} \otimes_{R} F_{i} ≃ R$ .

Remarks

The proof follows the route of GKS Lemma 3.11: the tensor product is the displayed three-term complex, its four-term middle term splits by the rank-one square, and two successive Gaussian eliminations cancel the two contractible two-term pieces; the two surviving directions are $R$ in degree $0$ . The two pivots use the middle-factor invariant decomposition; the two outer actions of $α_{i}$ are kept distinct. The ground field $Q$ makes the invariant decomposition available and all normalization scalars invertible. Rouquier's alternative proof of Lemma 3.3 uses the adjoint pairs attached to the split sequence $0 \to R^{s_{i}} \to R \to R^{s_{i}} (2) \to 0$ and Proposition 2.1 of the same paper; that route is not used here.

Depends on

Used by

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)