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.
A filtered quasi isomorphism detected on associated graded complexes
Example
Let and take , , , with zero other degrees. Filter it by for , and for . Give the weight-zero filtration, zero for and full for . The projection killing and fixing is a filtered quasi-isomorphism detected on associated-graded complexes.
Facts & Assumptions
Quasi isomorphism criterion from a filtered map proves that a map of degreewise finite filtered complexes which is a quasi-isomorphism on each graded complex is a quasi-isomorphism.
Abelian-group model for spectral-sequence computations supplies , finite coordinate groups and ordinary subgroup homology quotients.
Verification
Given: The two filtered complexes and the explicit projection in the example.
The differential squares to zero since the group below degree zero vanishes. The sole intermediate piece is a subcomplex, so the filtration on is by subcomplexes. The projection is a chain map: , and it preserves the specified pieces, including the zero lower tail and full upper tail. Both filtrations are finite in every degree, with the common bounds minus one and one.
On the map is the identity , hence an isomorphism on its sole homology group. On , the source is and the target is zero, because . The source has zero kernel in degree one and zero cokernel in degree zero, so the graded map is again a quasi-isomorphism. Every other graded complex is zero on both sides. Therefore all hypotheses of the finite branch of [F1] hold.
Apply [F1] to conclude that is a quasi-isomorphism. Directly, is injective with image , giving and via . The induced map is this same isomorphism, while all other homology maps are isomorphisms between zero groups. This checks the specific map rather than only the isomorphism type of the target. All coefficients, zero terms, filtration endpoints and one-dimensional graded pieces have been computed explicitly; no AC or splitting choice is required.
Depends on
Used by
Nothing in the library uses this result yet.
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
- Weibel, An Introduction to Homological Algebra, Chapter 5 (standard reference, not scraped)
- The Stacks Project, Homological Algebra (standard reference, not scraped)