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 filtered complex spectral sequence abuts to filtered homology
Statement
If the filtration on every is finite, the spectral sequence of the filtered chain complex stabilizes pointwise and naturally abuts to with its image filtration. This homology filtration is finite, exhaustive and separated. No uniform filtration bound in n is required.
Facts & Assumptions
Given: A filtered complex with a finite filtration on each chain object and fixed p,n.
Finite in degree n means and for some integers (Exhaustive separated bounded and finite filtration).
Graded homology is (The associated graded of filtered homology is a subquotient of chain level data).
The page transition is the natural inclusion-induced homology isomorphism (The next page is the homology of the current page).
Eventually stationary projected cycles and boundaries define (Limiting cycles boundaries and e infinity).
Finite support on each diagonal forces pointwise stabilization (Degree reasons force stabilization in a bounded region).
Abutment is a specified identification with the associated graded of filtered homology (Abutment to a filtered object).
Image pullbacks and quotient comparisons are canonical and natural (Spectral sequence subquotient and local lifting calculus).
Proof
Fix n,p and write , . Choose R≥1 so that and for every r≥R; [F1] supplies bounds in precisely these two degrees. Then and . Also , whose image is by the epic-pullback calculation [F7].
The page quotient is therefore stationary with value Its projected numerator and boundary subobjects are stationary too, giving exactly under [F4]. By [F2] this quotient is canonically . Separately the initial page on diagonal n vanishes outside , so [F5] supplies vanishing of both incident differentials and stabilization in the specified sense.
For , the cycle subobject is zero, so the image filtration on is zero. For it is Z, whose quotient map surjects onto ; hence . Thus the filtration is finite. A family containing 0 and has meet 0 and join by the subobject order, proving separation and exhaustiveness without infinite exactness.
A filtered chain map preserves the cycle and boundary subobjects in steps 1.1–2.1, and all quotient comparisons commute by [F7]. The page transitions [F3] were built from the same cycle inclusions; their stationary identifications agree with these comparisons. Thus the displayed isomorphisms form natural abutment data in the sense of [F6]. Each argument fixed n before using its finite bounds, so no common bounds over all degrees were needed.
Source notes
Stacks §12.24, Lemma 12.24.11 and equations 12.24.5.1–2; Weibel, bounded case of Theorem 5.5.1 pp.135–136. The chain proof explicitly uses degrees n−1 and n+1; no unbounded convergence clause is used.
Depends on
- Exhaustive separated bounded and finite filtration
- The associated graded of filtered homology is a subquotient of chain level data
- The next page is the homology of the current page
- Limiting cycles boundaries and e infinity
- Degree reasons force stabilization in a bounded region
- Abutment to a filtered object
- Spectral sequence subquotient and local lifting calculus
Used by
- Quasi isomorphism criterion from a filtered map Corollary
- The endpoints do not determine intermediate pages Counterexample
- A filtered complex collapsing at e one Example
- A nonzero d two differential in a small filtered complex Example
- Edge maps from a first quadrant spectral sequence Example
- The two step filtration and its spectral sequence Example
- Collapse solves all extension problems False statement
- Edge homomorphisms are natural Lemma
- Filtered convergence and the scope of the Ozsváth–Szabó construction Lemma
- Filtered instanton complex from the cube of knot resolutions Lemma
- Lee filtration, spectral sequence, and orientation classes Lemma
- Proper surjections have cohomological descent for constructible field sheaves Lemma
- Collapse does not in general split the abutment Proposition
- Shifting a filtered complex reindexes its spectral sequence Proposition
- A first quadrant filtered complex spectral sequence converges to filtered homology Theorem
- Acyclic assembly lemma for a first quadrant double complex Theorem
- Compact Kähler Hodge decomposition from elliptic harmonic forms Theorem
- Proper hypercovers compute constructible derived cohomology Theorem
- Termwise Hochschild spectral sequence of a bounded bimodule complex Theorem
- The cohomological filtered complex construction Theorem
- The column filtration spectral sequence of a first quadrant double complex Theorem
- The row filtration spectral sequence of a first quadrant double complex Theorem
Dependency tree · two levels
18 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
- Charles A. Weibel, An Introduction to Homological Algebra, Chapter 5 (standard reference, not scraped)
- Romyar Sharifi, Homological Algebra (standard reference, not scraped)