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 derived couple maps are well defined
Statement
The three maps of the derived-couple construction exist in every abelian category and are independent of all local preimages and cycle representatives. Their degrees are , and , respectively. No choice of global sections is needed.
Facts & Assumptions
Derived exact couple gives the image and homology quotient objects and the proposed formulas.
Exact couple gives , , and the consecutive zero composites.
Spectral sequence subquotient and local lifting calculus permits epic local lifting, descent of subobject membership and unique quotient maps.
Proof
Given: A page- exact couple. All expressions below are at a fixed homogeneous component with the typed shifts in [F1]; local lifts mean epic pullbacks as in [F3].
If is locally , then lies in . Descent of this membership shows that restricted to factors through the target . Its factorization is unique because that inclusion is monic. This defines without any preimage choice.
The composite lands in since . Follow it by . This map kills : an arrow into locally has form , and its image is . Hence it descends through to , uniquely. Explicitly, if locally, then after a further epic pullback, so . Thus its formula is independent of the preimage.
On , the map lands in , because . Changing a cycle representative by a boundary changes its image by . Thus this restricted map kills the boundary image and descends uniquely to . Equality after the epic cycle quotient also proves independence for arbitrary maps into , not just element representatives.
For the degree remains . To compute on , its local -preimage is at and sends it to , giving degree . The cycle restriction and quotient for preserve the original degree . The constructions above still apply when any image or homology object is zero, and for give . Every lift was a finite local epic pullback used to prove a canonical factorization; no global representative selection or AC was used.
Depends on
Used by
- The derived couple is exact Theorem
Cited to discharge well-definedness by Derived exact couple.
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, Lemma 12.21.2; full descent argument supplied here (standard reference, not scraped)