TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-26 (gpt-6-sol)

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.

Cellular homology computes singular homology

Statement

For every CW complex $X$ , abelian group $G$ , and $n \geq 0$ , the cellular complex has an isomorphism $H_{n}^{c e l l} (X; G) ≅ H_{n} (X; G)$ , natural with respect to cellular maps.

Facts & Assumptions

Given: A CW complex $X$ , an abelian group $G$ , and $n \geq 0$ . Write $X^{- 1} = \emptyset$ , suppress $G$ in homology notation, and write $C_{m} = H_{m} (X^{m}, X^{m - 1}; G)$ .

[F1]

Consecutive relative skeletal homology is concentrated in the cell dimension (Relative homology of consecutive CW skeleta).

[F2]

Each skeletal pair has its long exact homology sequence (Long exact sequence of a pair).

[F3]

Skeletal inclusions induce isomorphisms in degrees below the old skeleton dimension (Skeletal homology stabilizes away from the cell dimension).

[F4]

Every continuous image of a compact space in a CW complex with its supplied characteristic maps lies in a finite CW subcomplex, without a choice premise (Compact CW images have finite cell support without choice).

[F5]

Cellular homology is $\ker d_{n} / im d_{n + 1}$ (Cellular homology); $d_{m} = i_{m - 1} \partial_{m}$ , where $\partial_{m} : C_{m} \to H_{m - 1} (X^{m - 1})$ is the pair connecting map and $i_{m - 1} : H_{m - 1} (X^{m - 1}) \to C_{m - 1}$ is the relative quotient map (Cellular boundary from three consecutive skeleta).

Proof

technique · direct

1.1F1F2given

For every finite $m \geq 0$ , $H_{k} (X^{m}) = 0$ when $k > m$ : begin with the discrete $X^{0}$ case of [F1], and use [F2] successively with [F1] to pass from $X^{m - 1}$ to $X^{m}$ . The empty skeleton also has zero homology.

2.1F2F5step 1.1algebra

For $n \geq 1$ , the exact sequence of $(X^{n}, X^{n - 1})$ and step 1.1 give an injection $i_{n} : H_{n} (X^{n}) \to C_{n}$ with image $\ker \partial_{n}$ . The same argument one degree lower makes $i_{n - 1}$ injective, including $i_{0} : H_{0} (X^{0}) \to H_{0} (X^{0}, \emptyset)$ , which is an isomorphism. Since $d_{n} = i_{n - 1} \partial_{n}$ , we obtain $\ker d_{n} = \ker \partial_{n} = i_{n} H_{n} (X^{n})$ . For $n = 0$ this identity follows directly from $i_{0}$ being an isomorphism and $d_{0} = 0$ .

3.1F1F2F5step 2.1algebra

For $(X^{n + 1}, X^{n})$ , exactness and $H_{n} (X^{n + 1}, X^{n}) = 0$ give the exact tail $C_{n + 1} \overset{\partial_{n + 1}}{\to} H_{n} (X^{n}) ⟶ H_{n} (X^{n + 1}) ⟶ 0.$ Under the injection $i_{n}$ of step 2.1, $im \partial_{n + 1}$ corresponds exactly to $im d_{n + 1}$ by [F5]. Taking the quotient therefore yields $H_{n}^{c e l l} (X; G) ≅ H_{n} (X^{n}) / im \partial_{n + 1} ≅ H_{n} (X^{n + 1}; G) .$

4.1F3F4step 3.1

By [F3], all inclusions after $X^{n + 1}$ induce isomorphisms on $H_{n}$ . Each singular cycle is a finite sum of simplices; [F4] puts the image of each simplex in a finite subcomplex. Their finite union lies in some skeleton, so every class in $H_{n} (X; G)$ comes from a skeleton. If a skeletal cycle bounds in $X$ , its finite bounding chain likewise lies in some later skeleton, where that class already vanishes. Singular chain inclusions are injective, so these are respectively surjectivity and injectivity of the natural colimit map. Thus the colimit is $H_{n} (X; G)$ without any choice premise. Combining with step 3.1 proves the comparison for arbitrary, possibly infinite-dimensional, CW complexes.

5.1step 2.1step 3.1step 4.1given∎

A cellular map preserves all skeleta. Its induced chain maps commute with inclusions, quotient maps and connecting homomorphisms: the latter send a relative cycle represented by $c$ to the class of $\partial c$ , and a chain map commutes with $\partial$ . Consequently every injection, quotient identification and colimit map in steps 2.1--4.1 commutes with cellular maps. The comparison is therefore natural in exactly the stated sense.

Depends on

Used by

A CW complex with no cells in adjacent dimensions has zero cellular boundary Corollary
Morse Euler characteristic identity Corollary
A homology cobordism need not be an h-cobordism Counterexample
A nonorientable closed manifold has no integral fundamental class Counterexample
Steenrod squares do not all lift integrally Counterexample
The tautological line over RP∞ has no finite-rank complement Counterexample
Top squares do not determine lower squares Counterexample
Algebraic Lefschetz number via rational homology traces Definition
Euler characteristic of a compact manifold Definition
Lefschetz number of a finite CW self-map Definition
Cellular boundary matrix of a closed orientable surface Example
Cellular homology and ring-independent groups of complex projective space Example
Cellular homology of a lens space Example
Cellular homology of real projective space Example
Cohomology of lens spaces from UCT Example
Equal additive cohomology but different rings Example
Field cohomology of an infinite wedge of circles Example
Integral cohomology ring of a closed orientable surface Example
Integral cohomology ring of complex projective space Example
Kronecker pairing for a cellular circle generator Example
Mapping cone of a degree d circle map Example
Mod-two duality for real projective space Example
Period matrix and Jacobian of the pentagon curve Example
Real projective space shows coefficient-dependent perfectness Example
Serre spectral sequence of the complex Hopf fibration Example
Serre spectral sequence of the quaternionic Hopf fibration Example
Steenrod squares on real projective space Example
The complex projective plane has nonzero w2 and no Spin structure Example
A Bockstein class on RP-two times RP-four has nonzero integral Sq-three Lemma
A rational homology four-ball has square boundary torsion order Lemma
Admissible square actions have distinct leading monomials Lemma
Cellular homology of the one-polygon surface model Lemma
Cohomology ring of infinite complex projective space Lemma
Complex flag splitting with injective real pullback on smooth bases Lemma
Cyclic p-fold power construction Lemma
Every Whitehead class is realized by a finite CW homotopy equivalence Lemma
Finite surface normal forms, Jordan disks, and torsion control Lemma
Finite type and odd-primary acyclicity of K(F₂,q) Lemma
Finite-cellular cyclic squares agree with singular cup-i squares Lemma
Finite-cellular cyclic squares, Cartan formula, and cyclic-basis action Lemma

…and 30 more results.

Dependency tree · two levels

22 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

Allen Hatcher, Algebraic Topology, Theorem 2.35 (standard reference, not scraped)