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

Cancelling a generator with its inverse categorical twist

Example

Fix $m \geq 1$ and $1 \leq i \leq m$ , and let $R_{i} = [U_{i} \overset{β_{i}}{\to} A_{m}], R_{i}^{- 1} = [A_{m} \overset{γ_{i}}{\to} U_{i} {- 1}]$ be the twist complexes of The twist complexes R_i and R_i^{-1}, with $U_{i}$ in homological degree $- 1$ and $A_{m}$ in degree $0$ in the first complex, and $A_{m}$ in degree $0$ and $U_{i} {- 1}$ in degree $1$ in the second. The totalization $N : = R_{i} \otimes_{A_{m}} R_{i}^{- 1}$ of Signed totalization of graded A_m-bimodule actions is not the diagonal bimodule. Its three nonzero terms are $N^{- 1} = U_{i} \otimes_{A_{m}} A_{m} ≅ U_{i}, N^{0} = (U_{i} \otimes_{A_{m}} U_{i} {- 1}) \oplus (A_{m} \otimes_{A_{m}} A_{m}) ≅ (U_{i} \otimes_{A_{m}} U_{i} {- 1}) \oplus A_{m}, N^{1} = A_{m} \otimes_{A_{m}} U_{i} {- 1} ≅ U_{i} {- 1},$ so, counted with multiplicity, the tensor complex has the four terms $U_{i}$ in degree $- 1$ , then $U_{i} \otimes_{A_{m}} U_{i} {- 1}$ and $A_{m}$ in degree $0$ , then $U_{i} {- 1}$ in degree $1$ : it is not concentrated in degree $0$ . Writing $Q : =_{i} P \otimes_{A_{m}} P_{i} = Z u_{1} \oplus Z u_{2}$ with $u_{1} = e_{i} \otimes e_{i}$ in degree $0$ and $u_{2} = (i ∣ i - 1 ∣ i) \otimes e_{i}$ in degree $1$ , the differentials become the source's maps $\partial^{- 1} = (τ, β_{i}), \partial^{0} (z, a) = γ_{i} (a) - δ (z), τ (x \otimes y) = x \otimes u_{1} \otimes (i ∣ i - 1 ∣ i) y + x \otimes u_{2} \otimes y,$ $δ (x \otimes u_{1} \otimes y) = x \otimes y, δ (x \otimes u_{2} \otimes y) = x (i ∣ i - 1 ∣ i) \otimes y,$ where the middle tensor coordinate is the negative of the natural balanced identification with $P_{i} \otimes_{Z} Q \otimes_{Z}_{i} P {- 1}$ . This sign change converts the natural totalization maps $(- τ, β_{i})$ and $(δ, γ_{i})$ to the source’s displayed chart. The source's splitting of this totalization is $N ≅ T_{- 1} \oplus A_{m} \oplus T_{1},$ where $A_{m}$ is the diagonal bimodule in degree $0$ , and $T_{- 1}, T_{1}$ are the two two-term complexes $T_{- 1} = [U_{i} \overset{\partial^{- 1}}{\to} \partial^{- 1} (U_{i})], T_{1} = [P_{i} \otimes_{Z} Z u_{1} \otimes_{Z}_{i} P {- 1} \overset{- δ}{\to} U_{i} {- 1}],$ whose differentials are invertible; $T_{- 1}$ and $T_{1}$ are therefore contractible, with contracting homotopies the inverses $(\partial^{- 1})^{- 1}$ and $x \otimes y \mapsto - x \otimes u_{1} \otimes y$ of the displayed differentials. Thus the inverse pair cancels up to homotopy, not on the nose: the two contractible summands are the visible cost of the cancellation. The same holds with the factors in the opposite order.

Facts & Assumptions

Given: An integer $m \geq 1$ , an index $1 \leq i \leq m$ , the complexes $R_{i}, R_{i}^{- 1}$ with the maps $β_{i}, γ_{i}$ , the bimodule $U_{i}$ and its internal shift, the corner basis $e_{i} A_{m} e_{i} = Z e_{i} \oplus Z (i ∣ i - 1 ∣ i)$ , and the totalization of Signed totalization of graded A_m-bimodule actions.

[L1]

$R_{i} = [U_{i} \overset{β_{i}}{\to} A_{m}]$ with $U_{i}$ in degree $- 1$ and $A_{m}$ in degree $0$ , and $R_{i}^{- 1} = [A_{m} \overset{γ_{i}}{\to} U_{i} {- 1}]$ with $A_{m}$ in degree $0$ and $U_{i} {- 1}$ in degree $1$ ; both are bounded complexes of graded bimodules with two-sided finite graded projective terms and degree-zero differentials (The twist complexes R_i and R_i^{-1}).

[L2]

$R_{i} \otimes_{A_{m}} R_{i}^{- 1} ≃ A_{m}$ and $R_{i}^{- 1} \otimes_{A_{m}} R_{i} ≃ A_{m}$ via homotopy equivalences; the proof exhibits the splitting of the first tensor complex and the explicit maps $τ, δ, ξ$ (The generator complexes are mutually inverse).

[L3]

$β_{i} (e_{i} \otimes e_{i}) = e_{i}$ and $γ_{i} (1) = w_{i}$ with $w_{i}$ the four-term sum displayed in the Definition; $τ$ and $δ$ are the degree-zero bimodule maps with $δ τ = γ_{i} β_{i}$ , $δ ξ = γ_{i}$ , and the square (2.8) anticommutes (The Khovanov–Seidel bimodule maps β_i and γ_i, The generator complexes are mutually inverse).

[L4]

The totalization of two bounded complexes of graded bimodules has the terms $(R \otimes_{A_{m}} S)^{n} = ⨁_{p + q = n} R^{p} \otimes_{A_{m}} S^{q}$ and the differential $d (r \otimes s) = d_{R} r \otimes s + (- 1)^{p} r \otimes d_{S} s$ , and the tensor-unit maps $M \otimes_{A_{m}} A_{m} ≅ M$ , $A_{m} \otimes_{A_{m}} M ≅ M$ are canonical degree-zero isomorphisms (Signed totalization of graded A_m-bimodule actions).

[L5]

A two-term complex with invertible differential is contractible, with the inverse differential as contracting homotopy (Gaussian elimination splits a contractible two-term complex).

Verification

technique · direct

1.1L1L4

The four terms and their degrees. By [L4] the terms of $N = R_{i} \otimes_{A_{m}} R_{i}^{- 1}$ are the direct sums over $p + q = n$ of $R_{i}^{p} \otimes_{A_{m}} (R_{i}^{- 1})^{q}$ ; the nonzero pairs are $(p, q) = (- 1, 0), (0, 0), (- 1, 1), (0, 1)$ , giving the terms $U_{i}$ , $A_{m}$ , $U_{i} \otimes_{A_{m}} U_{i} {- 1}$ and $U_{i} {- 1}$ in homological degrees $- 1, 0, 0, 1$ as displayed, with the two degree- $0$ summands ordered as $U_{i} \otimes_{A_{m}} U_{i} {- 1}$ and $A_{m}$ ; the tensor-unit isomorphisms of [L4] identify the first and last with $U_{i}$ and $U_{i} {- 1}$ . This corrects the term count: there are four terms counted with multiplicity, not three $A_{m}$ 's.

2.1step 1.1L3L4

The differentials. After negating the natural identification of $U_{i} \otimes_{A_{m}} U_{i} {- 1}$ with $P_{i} \otimes_{Z} Q \otimes_{Z}_{i} P {- 1}$ and the tensor-unit identifications, the Koszul-signed differentials of [L4] take the form $\partial^{- 1} (u) = (τ (u), β_{i} (u))$ and $\partial^{0} (z, a) = γ_{i} (a) - δ (z)$ with the maps $τ, δ$ of the display: the component into $A_{m}$ is $β_{i}$ , the component into the middle bimodule is $τ$ , and the component out of $A_{m}$ is $γ_{i}$ , while the component out of the middle is $- δ$ after this coordinate change. Before that change the Koszul rule gives $(- τ, β_{i})$ and $(δ, γ_{i})$ , as required.

3.1step 2.1L3L5

The two contractible summands. The $u_{2}$ component of $τ$ is the identity on $U_{i}$ , so $\partial^{- 1}$ is injective and its restriction to its image is an isomorphism with inverse the $u_{2}$ -coefficient projection on the middle summand, so $T_{- 1}$ is contractible with contracting homotopy $(\partial^{- 1})^{- 1}$ by [L5]; the restriction $- δ ⁣ : P_{i} \otimes Z u_{1} \otimes_{i} P {- 1} \to U_{i} {- 1}$ is an isomorphism with inverse $x \otimes y \mapsto - x \otimes u_{1} \otimes y$ , so $T_{1}$ is contractible by [L5]. The map $a \mapsto (ξ (a), a)$ identifies the remaining graph in degree $0$ with $A_{m}$ with zero differential, because $\partial^{0} (ξ (a), a) = γ_{i} (a) - δ ξ (a) = 0$ .

4.1step 3.1L2∎

Conclusion of the example. By the direct sum decomposition of the generator lemma [L2], $N ≅ T_{- 1} \oplus A_{m} \oplus T_{1}$ ; by step 3.1 the outer summands are contractible, so $N$ is homotopy equivalent to the diagonal bimodule and $R_{i} R_{i}^{- 1} ≅ {Id}_{C_{m}}$ , while $N$ itself is a four-term complex and not equal to $A_{m}$ ; the same argument applies to $R_{i}^{- 1} \otimes_{A_{m}} R_{i}$ . The two contractible summands are exactly the cancellation cost, and their contracting homotopies are the displayed inverses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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, Proposition 2.4 (standard reference, not scraped)