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 = h_{0} (*)$ . For every $n \geq 0$ and $k \in Z$ , $h_{k} (D^{n}, S^{n - 1}) ≅ {\begin{cases} G & k = n, \\ 0 & k \neq n . \end{cases}$ At $n = 0$ the pair means $(*, \emptyset)$ . Also ${\tilde{h}}_{k} (S^{n}) ≅ 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 \neq \emptyset$ the correspondence gives $h_{n} (X, A) ≅ {\tilde{h}}_{n} (X / A)$ ; for $A = \emptyset$ it gives $h_{n} (X) ≅ {\tilde{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 \subset A \subset X$ there is a natural exact sequence $\dots \to h_{n} (A, B) \to h_{n} (X, B) \to h_{n} (X, A) \to h_{n - 1} (A, B) \to \dots$ , whose last map is the pair boundary followed by $h_{n - 1} (A) \to h_{n - 1} (A, B)$ . (Unreduced pair and reduced quotient axioms are equivalent on cw pairs)

Proof

1.1

The dimension axiom gives the assertion for $(*, \emptyset)$ . On $S^{0} = {-, +}$ the split augmentation is addition $h_{k} (*) \oplus h_{k} (*) \to h_{k} (*)$ , with kernel $g \mapsto (- g, g)$ . Thus the reduced sphere assertion starts in degree zero, with the displayed difference orientation.

F1algebra

2.1

For a nonempty sphere, the contractible cone has zero reduced groups. Its exact sequence identifies the relative cone group in degree $k$ with ${\tilde{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 ${\tilde{h}}_{k} (S^{n}) ≅ h_{k - n} (*)$ .

F1step 1.1

3.1

For $n \geq 1$ , apply the same cone boundary to $(D^{n}, S^{n - 1})$ . The dimension axiom makes $h_{k - n} (*)$ vanish unless $k = n$ , including all negative $k$ . Fix orientations by these boundary identifications starting with $(- g, g)$ on $S^{0}$ . They remain valid for $G = 0$ .

F1step 1.1step 2.1∎

Depends on

Unreduced pair and reduced quotient axioms are equivalent on cw pairs

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

May, A Concise Course in Algebraic Topology, 14§3, suspension corollaries, p.109; 15§2 p.120 (standard reference, not scraped)