Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

bounded finite length complex euler identities

Statement

For a bounded homological complex D of finite-length R-modules, i(1)iR(Di)=χ(D). If 0ABC0 is a short exact sequence of bounded complexes whose homology modules all have finite length, then χ(B)=χ(A)+χ(C). In this second assertion the terms need not have finite length. The shift D[1]i=Di1 with differential dD satisfies χ(D[1])=χ(D).

Facts & Assumptions

Given: A bounded complex D of finite-length R-modules; independently, a short exact sequence 0ABC0 of bounded complexes with finite-length homology. The shift convention is D[1]i=Di1 with differential dD.

[F1]

Euler characteristic is the alternating sum of homology lengths: koszul euler characteristic and degree indexed multiplicity.

[F2]

Finite length and length additivity in short exact sequences are supplied by Module length is additive in short exact sequences.

[F3]

A short exact sequence of complexes gives a long exact homology sequence: The long exact sequence in homology.

Proof

technique · direct
1.1

Set Zi=ker(di) and Bi=im(di+1). There are short exact sequences 0ZiDiBi10 and 0BiZiHi(D)0, with maps induced by the differential and quotient. Since Di has finite length, all these modules do. Additivity gives R(Di)=R(Hi(D))+R(Bi)+R(Bi1).

F2given
1.2

For any finite exact sequence 0E0Et0 of finite-length modules, set Jj to be the image in Ej, so J0=Jt+1=0 and 0JjEjJj+10 is exact. Hence R(Ej)=R(Jj)+R(Jj+1), and summation with alternating signs cancels every image length, yielding j(1)jR(Ej)=0.

F2algebra
2.1

Choose integers ab with Di=0 outside [a,b]. Then Ba1=Bb=0. In the alternating sum of the preceding equality, R(Bj) has coefficient (1)j+(1)j+1=0. Only i=ab(1)iR(Hi(D)) remains. This equals χ(D), including the zero complex and a complex with only one nonzero term.

F1step 1.1
2.2

The long exact sequence for 0ABC0 has successive blocks Hi(A),Hi(B),Hi(C),Hi1(A). Boundedness permits cutting it between zero endpoints, and all its terms have finite length by hypothesis. The alternating signs on each block can be taken as (1)i,(1)i,(1)i: the next block starts with (1)i1, the opposite of the previous block's last sign. The exact-sequence cancellation therefore gives χ(A)χ(B)+χ(C)=0.

F1F3step 1.2
3.1

The shift differential has the same kernels and images as dD in the corresponding degrees, so Hi(D[1])=Hi1(D). Reindexing the finite Euler sum gives χ(D[1])=j(1)j+1R(Hj(D))=χ(D). These establish all three assertions.

F1step 2.1step 2.2algebra

Remarks

Source locator: Hochster, Math 615, printed pp.104–105, the two cycle/boundary short exact sequences and their alternating cancellation. The short-exact-complex assertion is derived explicitly from the local homology LES. No convergence or finite-length-of-terms assumption is added to that assertion.

Depends on

Used by

Dependency tree · two levels

14 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