LemmaStatement: AI-adaptedProof: 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.

Coefficient comparison on finite cw pairs

Statement

For ordinary homology theories $h, k$ and a specified isomorphism $u : h_{0} (*) \to k_{0} (*)$ , there is a unique natural equivalence on finite CW pairs normalized by $u$ and commuting with connecting homomorphisms.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

The ordered-simplex comparison for an ordinary homology theory on finite simplicial pairs is unchanged by finite subdivision. It is natural for every continuous map of finite simplicial pairs and commutes with pair connecting homomorphisms. (Subdivision compatible continuous polyhedral homology comparison)

[F2]

Every finite CW pair $(X, A)$ is homotopy equivalent as a pair to a finite simplicial pair $(∣ K ∣, ∣ L ∣)$ . In particular there are maps of pairs in both directions whose composites are homotopic to the identities through maps preserving the designated subspaces. (Finite cw pairs admit finite simplicial homotopy models)

[F3]

For ordinary theories $h, k$ as in def-unreduced-homology-theory-on-cw-pairs, a morphism $η : h \to k$ consists of homomorphisms $η_{n} (X, A) : h_{n} (X, A) \to k_{n} (X, A)$ , natural for all maps of CW pairs and all $n \in Z$ , satisfying $\partial^{k} η_{n} = η_{n - 1} \partial^{h}$ . For a specified homomorphism $u : h_{0} (*) \to k_{0} (*)$ , the morphism is coefficient-normalized by $u$ if $η_{0} (*) = u$ . A comparison equivalence has every component invertible and is normalized by a specified coefficient isomorphism. Neither the existence nor uniqueness of such an extension is part of this definition. (Coefficient normalized morphism of ordinary homology theories)

[F4]

For any abelian group $G$ , $H_{0} (*; G) ≅ G$ and $H_{n} (*; G) = 0$ for every integer $n \neq 0$ . For every set-indexed family of pairs the canonical map $⨁_{α} H_{n} (X_{α}, A_{α}; G) ⟶ H_{n} (⨆_{α} X_{α}, ⨆_{α} A_{α}; G)$ is an isomorphism. Together with the structural axioms, singular homology is an ordinary theory with coefficient group $G$ . (Singular homology satisfies dimension and arbitrary additivity)

[F5]

For finite simplicial pairs $(K, L)$ and any ordinary theory $h$ with coefficient group $G$ , ordered simplex classes identify $C_{*}^{h} (K, L) ≅ C_{*}^{s i m p} (K, L; Z) \otimes G,$ with the alternating face differential. Consequently they give a coefficient-normalized isomorphism $h_{n} (∣ K ∣, ∣ L ∣) \to H_{n} (∣ K ∣, ∣ L ∣; G)$ , natural for simplicial maps and compatible with pair boundaries. No flatness of $G$ is assumed. (Oriented simplex comparison for an ordinary homology theory)

Proof

1.1

Let $G = h_{0} (*)$ , $G^{'} = k_{0} (*)$ . Singular homology with either coefficient is an ordinary theory by F4. On a finite simplicial pair, F5 supplies coefficient-normalized isomorphisms from $h$ and $k$ to singular homology with $G$ and $G^{'}$ . By F1 these isomorphisms are natural for all continuous maps of finite simplicial pairs, not only simplicial maps, and commute with pair boundaries. The coefficient chain map $1 \otimes u$ is invertible and commutes with the boundary because the latter uses integer coefficients. Composing these comparisons gives $η$ normalized by $u$ on finite simplicial pairs.

F1F3F4F5

2.1

For a finite CW pair choose a finite simplicial homotopy model $a : P \to (X, A)$ with pair homotopy inverse $b$ , by F2, and define $η_{X, A} = k (a) η_{P} h (b)$ . Homotopy invariance makes $h (a), k (a)$ isomorphisms. If $a^{'} : P^{'} \to (X, A)$ is another model, compare by the continuous pair map $b^{'} a : P \to P^{'}$ . Naturality on polyhedra and the homotopy-inverse identities imply the two transported maps agree.

F1F2step 1.1

3.1

For a continuous map $f : (X, A) \to (Y, B)$ , insert the pair map $b_{Y} f a_{X}$ between the models in the preceding formula. Polyhedral naturality cancels the intervening homotopy-inverse composites and gives $k (f) η_{X, A} = η_{Y, B} h (f)$ . Pair-boundary compatibility follows in the same way by applying naturality of each pair sequence to $a$ and $b$ .

F1F3step 2.1

4.1

A normalized boundary-compatible morphism is forced on relative ordered simplices by their boundary isomorphisms and its prescribed value on vertices. It is then forced on direct sums of those cell groups by the inclusion maps, and on a finite simplicial pair by the skeletal lift rule: $ρ (y)$ must map to the corresponding $ρ$ of the image lift. Thus it coincides with the constructed comparison there. Transport along a model forces it on every finite CW pair. The empty pair gives only the zero map and a point gives exactly $u$ .

F1F2F3step 1.1step 2.1∎

Depends on

Used by

Dependency tree · two levels

16 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, 15§2, uniqueness theorem pp.119–120 (standard reference, not scraped)
Hatcher, Algebraic Topology, Theorem 2C.5 pp.182–184; Axioms for Homology p.161 (standard reference, not scraped)