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.

Long exact sequence of a pair in singular cohomology

Statement

For every subspace AX and abelian group G there is an exact sequence Hn(X,A;G)jHn(X;G)rHn(A;G)Hn+1(X,A;G). Here j comes from including the relative cochains, r is restriction, and the connector sends a cocycle class [a] to [δa~], for any cochain extension a~ of a to X. Negative groups are zero, so the sequence begins 0H0(X,A;G)H0(X;G)H0(A;G).

Facts & Assumptions

[F1]

Relative singular cochain complex identifies relative cochains with absolute cochains vanishing on simplices in A, and defines their cohomology quotient.

[F2]

Singular cochain complex with coefficients identifies cochains with arbitrary functions on simplices and uses positive precomposition coboundary; The singular coboundary squares to zero gives δ2=0.

[F3]

Singular cohomology is contravariantly functorial makes restriction a cochain map and supplies its induced map on cohomology.

Proof

Given: The pair and coefficients of the statement. Abbreviate the relative, absolute and subspace cochain complexes by D,C,E, respectively, and their differentials by δ.

1.1

In every degree, restriction r:CnEn is onto: extend a function on simplices in A by zero on all other simplices of X, using [F2]. Its kernel is exactly Dn by [F1], and j:DnCn is inclusion. These maps commute with δ by [F1] and [F3]. Thus 0DjCrE0 is termwise exact. Extension by zero is a linear degreewise section, and is not asserted to be a cochain map. For negative degrees the exact row consists of zeros.

F1F2F3
2.1

Let aEn be a cocycle and choose an extension a~ as in step 1.1. Then rδa~=δa=0, so δa~Dn+1; it is closed by δ2=0. Two extensions differ by an element dDn and their differentials differ by the relative coboundary δd. If a=a+δb, extend b to b~; then a~+δb~ extends a and has the same differential as a~. Combining the two observations proves representative independence. Sum extensions and integer multiples prove that [a]=[δa~] is a homomorphism.

F1F2step 1.1
2.2

At Hn(C), every relative class restricts to zero. Conversely if a cocycle c has [rc]=0, write rc=δb in En. Extend bEn1 to b~Cn1. Then cδb~ is a relative cocycle representing [c]. For n=0, b and its extension are zero, since negative cochains vanish; the same reasoning is valid. Hence this kernel is exactly the relative image.

F1F2step 1.1
3.1

At Hn(E), a global cocycle restricting to a has zero connecting class. Conversely if [a]=0, an extension has δa~=δd for some dDn. Then a~d is a cocycle of C restricting to a, so [a] lies in the restriction image. This proves exactness there in both directions.

F1step 1.1step 2.1
3.2

At Hn+1(D), a connecting representative δa~ is a coboundary in C, so its class maps to zero. Conversely if a relative cocycle d is a global coboundary d=δc, then rc is a cocycle of E since δrc=rd=0. Its connector, using the extension c, is [d]. This proves exactness at the third type of position. If this relative degree is zero, cC1=0 forces d=0, establishing the initial injection explicitly.

F1F2step 1.1step 2.1
4.1

All integer degrees and all three types of position are covered by steps 3.1, 2.2 and 3.2, proving the long exact sequence and its connector. If A=, then D=C and E=0, so the sequence consists of identity and zero maps. If A=X, then D=0 and restriction is identity. Empty X or zero G give zero sequences. For a point and either of its two subspaces these same endpoint cases apply. The explicit extension-by-zero function is available without selecting any elements of G beyond its specified zero; no AC, projectivity or injectivity of G is used.

F1F2step 1.1step 2.1step 3.1step 2.2step 3.2

Depends on

Used by

Dependency tree · two levels

13 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