Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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 f:(X,A)(Y,B), meaning f(A)B, induces a contravariant map from the cohomology pair sequence for (Y,B) to that for (X,A), with every square commuting. In particular fY,B=X,A(fA):Hn(B;G)Hn+1(X,A;G). These maps satisfy identity and composition laws on pairs. Coefficient homomorphisms induce covariant maps of these sequences, commuting with pair pullbacks.

Facts & Assumptions

[F1]

Long exact sequence of a pair in singular cohomology gives inclusion, restriction and connector [a][δa~], independent of extension.

[F2]

Singular cohomology is contravariantly functorial gives precomposition cochain maps, identity/composition laws and commuting coefficient postcomposition maps.

[F3]

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 f, abelian coefficients G, and a coefficient homomorphism u:GG when considering coefficient naturality.

1.1

If a cochain φ on Y vanishes on simplices in B, then φf# vanishes on simplices in A, since their composites have image in B. Thus the cochain pullback of [F2] restricts to C(Y,B;G)C(X,A;G). It commutes with the differential and so preserves relative cocycles and coboundaries, inducing f by [F3]. The literal composition and identity formulas from [F2] restrict to these subcomplexes, hence hold on their quotient cohomology.

F2F3
1.2

The square with relative inclusion commutes because both composites send φ to φf# viewed as an absolute cochain. The restriction square commutes since restricting φf# to a simplex σ in A gives φ(fσ), also the value of (fA)(φB) on σ. Equality on simplices is equality of cochains by linear extension. These squares descend to cohomology.

F1F2F3
1.3

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 a~ extends a, then ua~ extends ua and δ(ua~)=uδa~; therefore it also commutes with the connector of [F1]. Finally u(φf#)=(uφ)f# proves commutation with pair pullback, and coefficient identity/composition laws restrict from [F2].

F1F2F3
2.1

For a cocycle a on B, let a~ be any extension to Y, available by [F1]. The cochain a~f# extends (fA)a on A. Its differential is (δa~)f# 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.

F1F2step 1.1step 1.2
3.1

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 A= or A=X, and likewise for B, the inclusion/restriction identities agree with the endpoint sequences of [F1] whenever f is a map of pairs. Empty X, 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.

F1F2F3step 1.1step 1.2step 2.1step 1.3

Depends on

Used by

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