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.
Failure of separatedness or completeness can destroy the claimed abutment
Statement
Failure of separatedness or completeness can invalidate recovery of a claimed target from the limiting page. There is a nonseparated filtered complex with nonzero homology and every spectral page zero. There is a separated exhaustive, but incomplete, filtered complex with and nonzero homology. An object and its completion can also have the same associated-graded spectral pages and nonisomorphic homology targets. All three examples below are choice-free.
Facts & Assumptions
Countable sequence groups and tail filtrations gives , the finite-support group , their tails , quotients , separatedness, completions and different cardinalities.
Abelian-group model for spectral-sequence computations licenses the abelian-group complexes and their subgroup kernels and coset homology quotients.
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 initial page, induced differential and homology transitions.
Induced filtration on homology uses actual homology images. Weak convergence of a spectral sequence identifies only the graded target; Strong convergence of a spectral sequence additionally requires separation and completeness.
Proof
Given: The groups in [F1]. All omitted chain degrees are zero.
Put with zero differential and for every integer . Each graded quotient is , so and every later page is zero by successive homology. But and every homology filtration term equals , whose intersection is nonzero. The zero limiting page agrees with the zero associated graded of this target; it does not imply that the target is zero. Thus this is weak convergence without separatedness or strong convergence.
Next take , , with differential the inclusion. On either nonzero degree set for and for . The inclusion preserves every tail, so these are subcomplexes. The filtration is increasing and exhaustive because . Its intersection is zero in both degrees, but its degree-one completion map is the proper inclusion ; hence the filtered complex is incomplete.
For , the successive quotient in either nonzero chain degree is , by the coordinate map with zero-extension inverse. The induced differential between these two graded terms is the identity of . For the quotient is zero. Thus every fixed- graded complex is either in degrees or the zero complex; its homology vanishes. Hence , and all later pages vanish. In contrast and ; the constant-one sequence gives a nonzero class because it is not finitely supported.
Every differs from its tail obtained by deleting coordinates by an element of . Thus is surjective for every , and the induced homology filtration has for every integer . This explains the lost target: the limiting zero page agrees with a zero associated graded, while the homology filtration is nonseparated. The chain complex's incompleteness was already checked in step 1.2; no complete-convergence theorem applies to it.
Finally take the zero-differential complexes and with the same tail filtrations. Their associated-graded terms are at for each , and zero elsewhere. Every spectral differential is zero because the chain differential is zero, so these graded identifications persist on every page. Their homology targets are respectively and , which are not isomorphic even as sets by [F1]. The inclusion induces the page isomorphisms and is the completion map, but is not onto on homology. Thus equal graded pages cannot replace the missing completeness hypothesis. The initial level , zero positive levels and empty deleted prefix all satisfy the displayed formulas. Every construction uses fixed coordinates or finite truncations, without AC.
Depends on
Used by
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)