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.
Excision for singular cohomology
Statement
If and , inclusion induces an isomorphism for every integer and every abelian coefficient group .
Facts & Assumptions
The cover-small inclusion is a chain homotopy equivalence proves the chain homotopy equivalence using the explicit integral operators in its proof, with least subdivision depths, , , and . In that construction every already-small simplex has , and lands in small chains.
Cover-small singular chains defines small chains for families whose interiors cover the space.
Relative singular cochain complex gives quotient integer chains and their dual relative cochains; Singular cochain complex with coefficients fixes the positive dual differential.
Naturality of the singular cohomology pair sequence identifies the map of relative cohomology induced by a pair inclusion as precomposition on these cochains.
Proof
Given: The subsets and coefficients of the statement. Put , and .
The interiors of and cover : a point outside lies outside , hence in the open set . Use this two-member family in [F2]. Its small subcomplex is , since its generators are precisely simplices whose image lies in one of the two members. The simplex subsets intersect exactly in those with image in , so the finite formal-chain model gives .
Use [F1]'s constructed maps and . Here every simplex in , and every simplex in , is already small. For such a simplex the least-depth recursion gives , so . Its faces are also small; hence from the explicit formula. Consequently , , and in particular both maps preserve . With inclusion the identities are and . These are the actual operators of the supplier proof, not an inference that an arbitrary homotopy inverse preserves subspaces.
Quotienting the identities in step 2.1 by yields maps and in reverse, with and . Step 1.1 identifies with : send a chain to its class modulo . This is onto since every element of is a sum of an chain and a chain, and its kernel is exactly the displayed intersection. The isomorphism commutes with boundaries, since all maps are induced by chain inclusions and quotients. Thus is the actual relative-chain inclusion for excision.
Precompose with and to obtain cochain maps and . The identity gives . On a degree- cochain on , put , with . The other identity in step 3.1 gives For a cocycle the right side is a coboundary; therefore both induced composites are identities on cohomology. This proves bijectivity, with inverse induced by , for arbitrary ; no exactness property of the Hom functor has been assumed.
By [F4] and step 3.1 the map just proved invertible is precisely the claimed restriction map, proving the theorem. If it is the identity; if , both relative complexes are zero; if , the hypothesis forces . Empty spaces, a point, zero coefficients and negative degrees are included. Degree zero in step 4.1 uses , so the homotopy formula has its correct zero first summand. The least-depth construction in [F1] and all quotient/dual formulas are specified without any choice of bases or representatives; no AC, flatness or coefficient injectivity is used.
Depends on
Used by
- Singular cohomology satisfies the Eilenberg Steenrod cohomology axioms Corollary
- Integral cohomology ring of complex projective space Example
- Mod-two cohomology ring of real projective space Example
- A manifold exhaustion passes duality to the colimit Lemma
- Cap product and the Mayer–Vietoris duality ladder Lemma
- Alexander duality for compact locally contractible subsets of a sphere Theorem
- Fully relative Poincaré–Lefschetz duality Theorem
- Poincaré–Lefschetz duality 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
- Hatcher, section 3.1, Excision, printed pages 201–202 (standard reference, not scraped)