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
- Chern class of tautological and hyperplane lines on complex projective space Example
- Euler class of the universal oriented two-plane Example
- 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
- A rational homology ball bounded by L(4,1) Lemma
- Cap product and the Mayer–Vietoris duality ladder Lemma
- Collared gluing has relative excision and evaluation maps Lemma
- First Chern form agrees with the topological line class Lemma
- Mod-two cohomology ring of infinite real projective space Lemma
- Mod-two cohomology rings of complex projective spaces Lemma
- Modification preserves open cohomology images Lemma
- Oriented real two-plane splitting with real-cohomology injection Lemma
- Pullback of the Thom class along a transverse section computes the Euler class Lemma
- The normal Thom class realizes the Poincare dual of a closed submanifold Lemma
- The tangent bundle of complex projective space and its Pontryagin classes Lemma
- The Thom quotient identifies relative and reduced cohomology Lemma
- Bocksteins are natural and stable Proposition
- Collapse pulls the Thom class back to the Poincaré dual Proposition
- Steenrod normalization, instability, suspension, and top square Proposition
- Alexander duality for compact locally contractible subsets of a sphere Theorem
- Cellular cochains compute cohomology with local coefficients Theorem
- Cohomological Serre spectral sequence Theorem
- Excision and Mayer–Vietoris with local coefficients Theorem
- Fully relative Poincaré–Lefschetz duality Theorem
- Poincaré–Lefschetz duality Theorem
- Reduced powers satisfy naturality, instability, Cartan, and Adem relations Theorem
- The geometric intersection number is the Poincare-dual cup pairing 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)