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.
An exhaustive nonseparated filtration with the wrong naive abutment
Statement refuted
It is false that an exhaustive filtered complex with zero limiting page must have zero actual homology. A nonseparated chain filtration gives one counterexample; an exhaustive separated but incomplete chain filtration gives another.
Facts & Assumptions
Abelian-group model for spectral-sequence computations supplies and subgroup homology quotients. Countable sequence groups and tail filtrations supplies , tails and the proper completion .
R page of the spectral sequence of a filtered complex, The filtered differential induces d r on the r page and The next page is the homology of the current page give the graded page, its differential and successive homology pages.
Induced filtration on homology uses images in actual homology. Failure of separatedness or completeness can destroy the claimed abutment distinguishes these failures from legitimate weak graded identifications.
Counterexample
Given: First with at every integer index; second the inclusion complex with for and full positive pieces.
In the first example every graded quotient is , so every page is zero. But and for every , by the identity inclusion of the whole subcomplex. Its filtration is exhaustive, nonseparated, and has zero associated graded. Thus its zero limiting page can identify with its zero graded homology without implying zero homology. The filtration is not finite, since no piece is zero.
In the second example the inclusion preserves every tail, so the pieces are subcomplexes. Both chain filtrations are exhaustive ( is full) and separated, but the degree-one completion map is the nonsurjective . At each of the degree-one and degree-zero graded groups is via coordinate , and the graded differential is the identity. At both graded groups are zero. Therefore and every later page vanishes.
The inclusion is injective, so , while . The constant-one sequence represents a nonzero class. For any and any , delete its first coordinates to obtain . The difference has finite support, so in . Thus the homology image of every tail subcomplex is all of , and at every index. The chain filtration was separated, but its homology filtration is not. This example fails chain completeness and finite bounds; the first fails separation already on chains. Neither is a counterexample to a theorem that requires these missing hypotheses. Empty deleted prefixes at , zero other degrees and every positive filtration index obey the same calculations, without AC.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
7 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)