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.
The two spectral sequences of a two by two double complex
Example
Put in all four positions . Let , , and let every vertical map and every other component be zero. The two spectral sequences have different early pages and different degree-one filtration jumps, but both compute , , with all other total homology zero.
Facts & Assumptions
The row filtration spectral sequence of a first quadrant double complex computes horizontal homology first, with and the row cutoff in vertical index.
The column filtration spectral sequence of a first quadrant double complex computes vertical homology first, with and the column cutoff in horizontal index.
Abelian-group model for spectral-sequence computations supplies the binary group and coordinate finite biproducts and homology quotients.
Verification
Given: The displayed two-by-two data. Every horizontal square is zero and every mixed composite includes a zero vertical map, so the double-complex identities hold.
In the column sequence the vertical differential is zero, so consists of the four copies of . Its is identity from to and zero from to . Thus is at and zero elsewhere. No higher differential has both source and target among those two positions, so these are also the limiting terms.
In the row sequence, the row with vertical index one is the identity complex and has zero homology. The row with vertical index zero has zero horizontal differential, so its two homology terms are . With the required transposition these lie at spectral positions . The induced vertical is zero, and all later differentials have zero endpoints. Thus this page is already stationary.
Order total degree one as . Then the total complex is in degrees . The first map is injective, its image is , and the second map has kernel and zero image. Consequently , by the first coordinate, and . Other degrees are zero.
The surviving class is represented by . Row cutoff zero already includes it, giving and . Column cutoff zero includes only the degree-one summand , whose class in total homology is zero, so and . This accounts for the limiting positions versus despite the common total target. The first-quadrant finite bounds, axes and all omitted zero degrees have been checked; no representatives or maps were selected using AC.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
3 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
- Weibel, An Introduction to Homological Algebra, Chapter 5 (standard reference, not scraped)
- The Stacks Project, Homological Algebra (standard reference, not scraped)