Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Any ordinary homology theory computes relative cell groups from its coefficient group

Statement

Let h be an ordinary theory with coefficient group G=h0(∗). For every n≥0 and k∈Z, hk(Dn,Sn−1)≅{Gk=n,0k≠n. At n=0 the pair means (∗,∅). Also h~k(Sn)≅G for k=n and zero otherwise, including n=0. Choose the disk identifications by ordered orientations and iterated cone boundaries, so they commute with these boundaries.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

Ordinary unreduced theories on CW pairs and reduced ordinary theories on based CW spaces with vertex basepoints determine one another, naturally and compatibly with morphisms and coefficients. For A≠∅ the correspondence gives hn(X,A)≅h~n(X/A); for A=∅ it gives hn(X)≅h~n(X+), where X+=X⊔{∗}. Under this correspondence, pair boundaries are cofiber boundaries followed by inverse suspension, and arbitrary disjoint-sum additivity corresponds to arbitrary wedge additivity. For a CW triple B⊂A⊂X there is a natural exact sequence ⋯→hn(A,B)→hn(X,B)→hn(X,A)→hn−1(A,B)→⋯, whose last map is the pair boundary followed by hn−1(A)→hn−1(A,B). (Unreduced pair and reduced quotient axioms are equivalent on cw pairs)

Proof

1.1F1algebra

The dimension axiom gives the assertion for (∗,∅). On S0={−,+} the split augmentation is addition hk(∗)⊕hk(∗)→hk(∗), with kernel g↦(−g,g). Thus the reduced sphere assertion starts in degree zero, with the displayed difference orientation.

2.1F1step 1.1

For a nonempty sphere, the contractible cone has zero reduced groups. Its exact sequence identifies the relative cone group in degree k with h~k−1 of its base, including degree one where this is a reduced zero-degree group. The quotient is the suspension sphere. Iterating F1's natural suspension gives h~k(Sn)≅hk−n(∗).

3.1F1step 1.1step 2.1∎

For n≥1, apply the same cone boundary to (Dn,Sn−1). The dimension axiom makes hk−n(∗) vanish unless k=n, including all negative k. Fix orientations by these boundary identifications starting with (−g,g) on S0. They remain valid for G=0.

Depends on

Used by

Dependency tree · two levels

4 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