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 column filtration spectral sequence of a first quadrant double complex
Statement
For a first-quadrant homological double complex , the column filtration of has Its differentials have bidegree , and The target filtration is finite in each degree.
Facts & Assumptions
Row and column filtrations of a first quadrant double complex specifies both cutoffs and their finite biproduct total objects.
The row filtration spectral sequence of a first quadrant double complex computes the row pages, differential and finite image-filtration abutment.
The next page is the homology of the current page supplies natural page transitions; Bounded filtered complex spectral sequence abuts to filtered homology supplies natural abutment identifications; Induced filtration on homology defines the target as an image.
Proof
Given: The first-quadrant complex in the statement, with anticommuting arrows .
Define , with and . The two square-zero identities for are those for respectively, and its mixed sum is the mixed sum for with the two summands exchanged. Thus is again a first-quadrant anticommuting double complex. In each total degree, permutation of the finite summands gives an isomorphism . It commutes with total differentials because it changes into . The row cutoff in becomes the column cutoff in .
Apply the row theorem to . Its horizontal homology at is , and its induced vertical differential is the original . Its second page is therefore , with the same filtered bidegrees. These are the pages of the column-filtered : the filtration-preserving isomorphism in step 1.1 identifies their graded objects and differentials, and natural page transitions propagate the identification through every page. No sign twist is needed in the transposition.
The same filtered isomorphism sends to , hence sends their images to each other. Naturality of finite convergence identifies the stationary page in step 2.1 with the stated associated graded of these images. The bounds are and for ; for negative the complex is zero. This includes , a zero complex and a complex in one column. All maps are specified by finite permutations and universal properties, so no choice assumption enters.
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
Dependency tree · two levels
5 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 (homological anticommuting convention) (standard reference, not scraped)