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 row filtration spectral sequence of a first quadrant double complex
Statement
For a first-quadrant homological double complex , the row filtration of has a spectral sequence with The differential on page has bidegree , and the stationary page identifies canonically with This target filtration is finite in each total degree. Horizontal homology is taken first; the spectral first coordinate is the original vertical index.
Facts & Assumptions
Row and column filtrations of a first quadrant double complex gives the finite row cutoff and associated graded with differential .
The next page is the homology of the current page gives the natural page transition .
The filtered differential induces d r on the r page gives bidegree and the local rule .
Spectral sequence subquotient and local lifting calculus licenses local representatives after epic pullback and descent of maps preserving numerator and denominator.
Bounded filtered complex spectral sequence abuts to filtered homology proves natural abutment for degreewise finite filtrations; Induced filtration on homology specifies the image filtration.
Proof
Given: as stated, with and .
The row- quotient of total degree is . The arrow stays in this row and enters the preceding row, which is zero in the quotient. Thus and . This remains valid when either index is negative, as the component is then zero.
Taking homology gives . A horizontal cycle has total differential , so the page-one rule gives . This is a well-defined horizontal homology class: , and if changes by then changes by , a horizontal boundary. In an abelian category these calculations mean preservation of kernel and image subobjects; they may be checked after epic pullback and descend uniquely. No global representatives are selected.
Since , the induced page-one arrows square to zero, and their homology is precisely . The next-page isomorphism therefore gives the displayed . Both and all later subquotients vanish off the first quadrant. The differential bidegrees are those of the filtered construction, , with no extra sign in because was already the total differential.
In degree , and ; negative degrees are zero. Thus the bounded-filtration theorem applies degree by degree to this spectral sequence and identifies its stationary page with the associated graded of the displayed image filtration. That filtration is zero at and all of at for . For there is only one possible quotient, and for the zero complex all pages and quotients are zero. The argument uses no infinite exactness or AC.
Depends on
Used by
- The two spectral sequences of a two by two double complex Example
- The two spectral sequences of a double complex have identical e one pages False statement
- The two double complex spectral sequences have the same abutment but not the same pages Proposition
- Acyclic assembly lemma for a first quadrant double complex Theorem
- The column filtration spectral sequence of a first quadrant double complex Theorem
Dependency tree · two levels
4 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, Lemmas 12.25.1 and 12.25.3 (translated conventions; calculation supplied here) (standard reference, not scraped)