Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27
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.

Totalizing a two-term twist action

Example

Fix m≥1 and 1≤i≤m, let Ri=[Ui→βiAm] be the twist complex of The twist complexes R_i and R_i^{-1}, with Ui in homological degree −1 and Am in homological degree 0, and let X=[ X−1→ d X0 ] be a two-term complex of finitely generated graded projective left Am-modules, concentrated in homological degrees −1 and 0 with d of internal degree 0. Then the signed totalization Ri⊗AmX of Signed totalization of graded A_m-bimodule actions has exactly four tensor summands, distributed over three homological degrees: (Ri⊗AmX)−2=Ui⊗AmX−1,(Ri⊗AmX)−1=(Ui⊗AmX0)⊕(Am⊗AmX−1),(Ri⊗AmX)0=Am⊗AmX0, with differentials d−2(r⊗x)=βi(r)⊗x−r⊗dx,d−1(r⊗y)=βi(r)⊗y,d−1(a⊗x)=a⊗dx,d0=0, for r⊗x∈Ui⊗AmX−1, r⊗y∈Ui⊗AmX0 and a⊗x∈Am⊗AmX−1. The two routes from the bottom degree to the top degree cancel: with the sign (−1)−1=−1 attached to the column Ui, the composite d−1d−2 sends r⊗x first to βi(r)⊗x−r⊗dx and then to βi(r)⊗dx−βi(r)⊗dx=0.

Facts & Assumptions

Given: An integer m≥1, an index 1≤i≤m, the bimodule Ui with the degree-zero bimodule map βi:Ui→Am, the twist complex Ri=[Ui→βiAm] with Ui in degree −1 and Am in degree 0, and a two-term complex X of finite graded projective left Am-modules with terms X−1,X0 and degree-zero differential d.

[L1]

For a bounded complex R of graded (Am,Am)-bimodules and a bounded complex X of graded left Am-modules the totalization has (R⊗AmX)n=⨁p+q=nRp⊗AmXq and total differential d(r⊗x)=dRr⊗x+(−1)pr⊗dXx for r in homological degree p; the sign uses the homological degree of the first factor and never its internal degree (Signed totalization of graded A_m-bimodule actions).

[F2]

βi:Ui→Am is a degree-zero map of graded (Am,Am)-bimodules, and the only nonzero differential of Ri is βi, Ri1=0 and Rin=0 for n≠−1,0 (The twist complexes R_i and R_i^{-1}, The Khovanov–Seidel bimodule maps β_i and γ_i).

[F3]

X has Xn=0 for n≠−1,0 and dX−1=d, with dX0=0 because there is no term in degree 1; d is a degree-zero Am-linear map (Signed totalization of graded A_m-bimodule actions).

[L4]

For a graded ring R and a graded left R-module N the unit map R⊗RN→N, r⊗n↦rn, is a degree-zero isomorphism, so the summands Am⊗AmXq may be read as Xq (Graded associativity, units, and internal-shift tensor isomorphisms).

Proof

technique · direct
1.1

The four summands and their degrees. Since Ri has its two terms in degrees −1 and 0 by [F2] and X has its two terms in degrees −1 and 0 by [F3], the index pairs (p,q) with both Rip and Xq nonzero are (−1,−1),(−1,0),(0,−1),(0,0), and the diagonal ⨁p+q=n of [L1] collects them as p+q=−2 for (−1,−1), as p+q=−1 for (−1,0) and (0,−1), and as p+q=0 for (0,0); this gives the three displayed degrees with the four tensor summands Ui⊗AmX−1, Ui⊗AmX0, Am⊗AmX−1, Am⊗AmX0.

F2F3L1
1.2

The differentials. By [L1] the differential on Ui⊗AmX−1 is dR⊗1+(−1)−11⊗dX=βi⊗1−1⊗d, which on an elementary tensor is r⊗x↦βi(r)⊗x−r⊗dx, and the differential on Ui⊗AmX0 is βi⊗1+(−1)−11⊗dX=βi⊗1, since dX=0 on X0 by [F3]; the differential on Am⊗AmX−1 is 0+(−1)01⊗d=1⊗d, that is a⊗x↦a⊗dx, and on Am⊗AmX0 it is 0 because Ri1=0 and dX0=0. No internal degree enters any sign, and all four maps preserve the total internal degree because βi and d are degree-zero maps by [F2] and [F3].

F2F3L1
2.1

The two routes cancel. For r⊗x∈Ui⊗AmX−1 step 1.2 gives d−2(r⊗x)=βi(r)⊗x−r⊗dx, an element of the two summands of degree −1; applying d−1 to the two pieces separately gives d−1(βi(r)⊗x)=βi(r)⊗dx in the first summand and d−1(−r⊗dx)=−βi(r)⊗dx in the second, the latter because d−1 on Ui⊗AmX0 is βi⊗1 and dX(dx)=0; the two results are negatives of one another, so d−1d−2=0 on the bottom term, and d0d−1=0 holds trivially because d0=0. Hence the four displayed maps make the totalization a complex, as [L1] guarantees in general.

step 1.2L1
2.2

Unit form of the two upper summands. By [L4] the summands Am⊗AmX−1 and Am⊗AmX0 are degree-zero isomorphic to X−1 and X0 through the multiplication maps, so the middle term of the totalization may be written as X−1⊕(Ui⊗AmX0) and the top term as X0, with the differentials x↦dx and the Ui-component βi⊗1 respectively.

step 1.2L4
3.1

Conclusion. A two-term twist complex Ri and a two-term projective complex X produce the totalization Ui⊗AmX−1→(Ui⊗AmX0)⊕(Am⊗AmX−1)→Am⊗AmX0 with the four summands and the differentials of step 1.2, whose square vanishes by the explicit cancellation of step 2.1, and whose two Am-columns may be read as X−1 and X0 by step 2.2. The sign −1 in the bottom differential is the Koszul sign (−1)p at p=−1, that is, it is attached to the homological degree of the first factor and not to any internal degree, which is the point of the construction.

step 1.2step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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