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 of finite-length -modules, If is a short exact sequence of bounded complexes whose homology modules all have finite length, then . In this second assertion the terms need not have finite length. The shift with differential satisfies .
Facts & Assumptions
Given: A bounded complex of finite-length -modules; independently, a short exact sequence of bounded complexes with finite-length homology. The shift convention is with differential .
Euler characteristic is the alternating sum of homology lengths: koszul euler characteristic and degree indexed multiplicity.
Finite length and length additivity in short exact sequences are supplied by Module length is additive in short exact sequences.
A short exact sequence of complexes gives a long exact homology sequence: The long exact sequence in homology.
Proof
Set and . There are short exact sequences and , with maps induced by the differential and quotient. Since has finite length, all these modules do. Additivity gives .
For any finite exact sequence of finite-length modules, set to be the image in , so and is exact. Hence , and summation with alternating signs cancels every image length, yielding .
Choose integers with outside . Then . In the alternating sum of the preceding equality, has coefficient . Only remains. This equals , including the zero complex and a complex with only one nonzero term.
The long exact sequence for has successive blocks . 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 : the next block starts with , the opposite of the previous block's last sign. The exact-sequence cancellation therefore gives .
The shift differential has the same kernels and images as in the corresponding degrees, so . Reindexing the finite Euler sum gives . These establish all three assertions.
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
- Stacks Project, 43.15.4–6; local proof with stated module-relative and coefficient conventions (standard reference, not scraped)
- Hochster, Math 615 Winter 2012, pp.104–108: Euler characteristics and the multiplicity theorem (standard reference, not scraped)