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.

Far commutativity of the generator complexes

Statement

Fix $m \geq 1$ and let $R_{i}$ and $R_{i}^{- 1}$ be the twist complexes of graded $(A_{m}, A_{m})$ -bimodules of The twist complexes R_i and R_i^{-1}, with $R_{i} = [U_{i} \overset{β_{i}}{\to} A_{m}]$ having $U_{i}$ in homological degree $- 1$ and $A_{m}$ in degree $0$ . If $∣ i - j ∣ > 1$ then there is an isomorphism of complexes of graded $(A_{m}, A_{m})$ -bimodules $R_{i} \otimes_{A_{m}} R_{j} ≅ R_{j} \otimes_{A_{m}} R_{i},$ and consequently an isomorphism of endofunctors of $C_{m}$ $R_{i} R_{j} ≅ R_{j} R_{i} .$

Facts & Assumptions

Given: An integer $m \geq 1$ , indices $i, j$ with $∣ i - j ∣ > 1$ , the two-term complexes $R_{i} = [U_{i} \overset{β_{i}}{\to} A_{m}]$ , $R_{j} = [U_{j} \overset{β_{j}}{\to} A_{m}]$ with $U_{i}, U_{j}$ in homological degree $- 1$ and the diagonal bimodule $A_{m}$ in degree $0$ in both, and the totalization of Signed totalization of graded A_m-bimodule actions.

[L1]

$U_{i} = P_{i} \otimes_{Z}_{i} P$ and $β_{i} : U_{i} \to A_{m}$ is the degree-zero bimodule map with $β_{i} (e_{i} \otimes e_{i}) = e_{i}$ ; both $R_{i}$ and $R_{j}$ are bounded complexes of graded $(A_{m}, A_{m})$ -bimodules with degree-zero differentials, the differential of $R_{i}$ being $β_{i}$ (The twist complexes R_i and R_i^{-1}, The Khovanov–Seidel bimodule maps β_i and γ_i).

[L2]

If $∣ i - j ∣ > 1$ then $U_{i} \otimes_{A_{m}} U_{j} = 0$ as a graded $(A_{m}, A_{m})$ -bimodule (Corner computations: the U_i satisfy the Temperley-Lieb relations).

[L3]

For bounded complexes $R, S$ of graded $(A_{m}, A_{m})$ -bimodules the totalization has $(R \otimes_{A_{m}} S)^{n} = ⨁_{p + q = n} R^{p} \otimes_{A_{m}} S^{q}$ with $d (r \otimes s) = d_{R} r \otimes s + (- 1)^{p} r \otimes d_{S} s$ ; it is a bounded complex, functorial in both variables, and its terms carry the bimodule structure inherited from the two factors (Signed totalization of graded A_m-bimodule actions).

[L4]

For every graded $(A_{m}, A_{m})$ -bimodule $M$ the tensor-unit maps $A_{m} \otimes_{A_{m}} M \to M$ , $a \otimes m \mapsto a m$ , and $M \otimes_{A_{m}} A_{m} \to M$ , $m \otimes a \mapsto m a$ , are degree-zero isomorphisms of graded bimodules (Graded associativity, units, and internal-shift tensor isomorphisms).

[L5]

A bounded complex of graded $(A_{m}, A_{m})$ -bimodules with two-sided finite graded projective terms acts on $C_{m}$ by an exact triangulated endofunctor, and an isomorphism of such complexes induces a natural isomorphism of the associated functors (Bounded two-sided projective bimodule complexes act on C_m).

Proof

technique · direct

1.1L1L2L3L4

The two totalizations are the same complex with the two factors interchanged. By [L3] the degree $- 2$ term of $R_{i} \otimes_{A_{m}} R_{j}$ is $U_{i} \otimes_{A_{m}} U_{j}$ , which is $0$ by [L2]; its degree $- 1$ term is $(U_{i} \otimes_{A_{m}} A_{m}) \oplus (A_{m} \otimes_{A_{m}} U_{j})$ and its degree $0$ term is $A_{m} \otimes_{A_{m}} A_{m}$ , with nothing else. Using the unit isomorphisms of [L4] to identify $U_{i} \otimes_{A_{m}} A_{m} ≅ U_{i}$ , $A_{m} \otimes_{A_{m}} U_{j} ≅ U_{j}$ and $A_{m} \otimes_{A_{m}} A_{m} ≅ A_{m}$ , the differential of [L3] reads $(u, v) \mapsto β_{i} (u) + β_{j} (v)$ : on $u \otimes 1$ the Koszul sign multiplies the zero second summand only, and on $1 \otimes v$ the first summand is zero and the sign is $(- 1)^{0} = 1$ . Hence $R_{i} \otimes_{A_{m}} R_{j}$ is isomorphic to the two-term complex $C_{i j} = [U_{i} \oplus U_{j} \overset{(β_{i}, β_{j})}{\to} A_{m}]$ with $U_{i} \oplus U_{j}$ in degree $- 1$ . Symmetrically $R_{j} \otimes_{A_{m}} R_{i} ≅ C_{j i} = [U_{j} \oplus U_{i} \overset{(β_{j}, β_{i})}{\to} A_{m}]$ .

2.1step 1.1L1

The flip is a chain isomorphism. The flip $s : U_{i} \oplus U_{j} \to U_{j} \oplus U_{i}$ , $s (u, v) : = (v, u)$ , is a degree-zero isomorphism of graded bimodules; together with the identity of $A_{m}$ it defines a degree-zero isomorphism of graded bimodule complexes $C_{i j} \to C_{j i}$ . It commutes with the differentials because $(β_{j}, β_{i}) \circ s = (β_{i} (u) + β_{j} (v))$ on $(u, v)$ equals the composite $s$ after $(β_{i}, β_{j})$ , the target being $A_{m}$ in both cases and no sign entering the degree-zero component.

3.1step 1.1step 2.1

Conclusion for the complexes. The composite of the identifications of step 1.1 with the flip of step 2.1 is an isomorphism of complexes of graded $(A_{m}, A_{m})$ -bimodules $R_{i} \otimes_{A_{m}} R_{j} ≅ R_{j} \otimes_{A_{m}} R_{i}$ .

4.1step 3.1L5

Conclusion for the functors. Both $R_{i} \otimes_{A_{m}} R_{j}$ and $R_{j} \otimes_{A_{m}} R_{i}$ are bounded complexes with two-sided finite graded projective terms, since the terms $A_{m}$ , $U_{i} \oplus U_{j}$ , $U_{j} \oplus U_{i}$ are finite graded projective on both sides; by [L5] the isomorphism of step 3.1 induces a natural isomorphism of the endofunctors $M \mapsto (R_{i} \otimes_{A_{m}} R_{j}) \otimes_{A_{m}} M$ and $M \mapsto (R_{j} \otimes_{A_{m}} R_{i}) \otimes_{A_{m}} M$ of $C_{m}$ . Composing with the canonical associativity identifications $(R_{i} \otimes_{A_{m}} R_{j}) \otimes_{A_{m}} M ≅ R_{i} \otimes_{A_{m}} (R_{j} \otimes_{A_{m}} M)$ and $(R_{j} \otimes_{A_{m}} R_{i}) \otimes_{A_{m}} M ≅ R_{j} \otimes_{A_{m}} (R_{i} \otimes_{A_{m}} M)$ gives the asserted natural isomorphism $R_{i} R_{j} ≅ R_{j} R_{i}$ .

5.1step 3.1step 4.1L1∎

Conclusion. For $∣ i - j ∣ > 1$ the vanishing $U_{i} \otimes_{A_{m}} U_{j} = 0$ collapses both tensor complexes to the two-term complexes $C_{i j}$ , $C_{j i}$ , the flip identifies them, and the induced natural isomorphism of functors is $R_{i} R_{j} ≅ R_{j} R_{i}$ , both sides being the two-term complexes of [L1]. No choice principle is used.

Depends on

Used by

Dependency tree · two levels

34 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

Mikhail Khovanov and Paul Seidel, Quivers, Floer Cohomology, and Braid Group Actions, J. Amer. Math. Soc. 15 (2002) 203-271, Theorem 2.5 and equation (2.10) (standard reference, not scraped)