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.
Naturality of the singular cohomology pair sequence
Statement
A continuous map of pairs , meaning , induces a contravariant map from the cohomology pair sequence for to that for , with every square commuting. In particular These maps satisfy identity and composition laws on pairs. Coefficient homomorphisms induce covariant maps of these sequences, commuting with pair pullbacks.
Facts & Assumptions
Long exact sequence of a pair in singular cohomology gives inclusion, restriction and connector , independent of extension.
Singular cohomology is contravariantly functorial gives precomposition cochain maps, identity/composition laws and commuting coefficient postcomposition maps.
Relative singular cochain complex identifies relative cochains with those vanishing on chains in the subspace and forms their cohomology quotient.
Proof
Given: The map of pairs , abelian coefficients , and a coefficient homomorphism when considering coefficient naturality.
If a cochain on vanishes on simplices in , then vanishes on simplices in , since their composites have image in . Thus the cochain pullback of [F2] restricts to . It commutes with the differential and so preserves relative cocycles and coboundaries, inducing by [F3]. The literal composition and identity formulas from [F2] restrict to these subcomplexes, hence hold on their quotient cohomology.
The square with relative inclusion commutes because both composites send to viewed as an absolute cochain. The restriction square commutes since restricting to a simplex in gives , also the value of on . Equality on simplices is equality of cochains by linear extension. These squares descend to cohomology.
Coefficient postcomposition preserves zero values on subspace chains and commutes with coboundaries by [F2]. Thus it gives maps on all three kinds of cohomology. It commutes with inclusions and restrictions by the pointwise definitions. If extends , then extends and ; therefore it also commutes with the connector of [F1]. Finally proves commutation with pair pullback, and coefficient identity/composition laws restrict from [F2].
For a cocycle on , let be any extension to , available by [F1]. The cochain extends on . Its differential is by [F2]. Hence both sides of the asserted connector square are represented by this same relative cocycle. Independence from the extension is precisely [F1], so the square commutes on cohomology. It is not necessary that pullback preserve the particular extension-by-zero section.
Steps 1.1, 1.2, 2.1 and 1.3 prove every square and both functorialities. In degree zero the connector still uses an extended zero-cocycle and the same calculation; negative groups and their maps are zero. For or , and likewise for , the inclusion/restriction identities agree with the endpoint sequences of [F1] whenever is a map of pairs. Empty , point spaces and zero coefficients are covered by these literal formulas. No global family of extensions is chosen: one may use the specified zero extension for the one cocycle under consideration, so no AC 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
- Local coordinate cup products generate top relative cohomology Lemma
- Excision for singular cohomology Theorem
Dependency tree · two levels
10 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, Induced Homomorphisms, printed page 201 (standard reference, not scraped)