CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Finite-range comparison with an arbitrary simply connected target

Statement

Assume AC. Let N≥2, X be a nonempty path-connected simply connected CW complex, Y an arbitrary nonempty path-connected simply connected space, and f:(X,x₀)→(Y,y₀) a based continuous map. If its integral homology maps are isomorphisms for 0≤i<N and surjective at N, its based homotopy maps are isomorphisms for 1≤i<N and surjective at N. No CW-type or ordinary product-CW hypothesis is required on Y.

Facts & Assumptions

Given: AC; an integer $N \geq 2$ ; a nonempty path-connected simply connected CW complex $X$ ; an arbitrary nonempty path-connected simply connected space $Y$ ; and a based continuous map $f : X \to Y$ whose integral homology map is an isomorphism for $0 \leq i < N$ and a surjection for $i = N$ .

[F1]

The relative CW-approximation theorem produces a CW complex $Z$ containing $X$ as a subcomplex and a weak equivalence $Q : Z \to Y$ restricting to a prescribed map on $X$ (CW approximation of an arbitrary space, Weak homotopy equivalence).

[F2]

A weak equivalence induces an isomorphism in integral singular homology (Weak homotopy equivalences induce integral homology isomorphisms without choice) and isomorphisms of all based homotopy groups, with a bijection on path components (Weak homotopy equivalence).

[F3]

The preceding CW comparison theorem applies to a based map of nonempty path-connected simply connected CW complexes with the stated homology hypotheses (Integral homology comparison gives finite-range homotopy comparison for simply connected CW complexes).

[F4]

AC is inherited from the CW comparison theorem [F3]; the relative CW approximation in [F1] assumes no choice principle (The Axiom of Choice).

Proof

technique · direct

1.1givenF1F2

Apply the relative clause of thm-cw-approximation-of-an-arbitrary-space directly to $f : X \to Y$ . It gives a CW complex $Z$ containing $X$ as a subcomplex and a weak equivalence $Q : Z \to Y$ whose restriction to $X$ is exactly $f$ . The weak-equivalence homology supplier makes $Q_{*}$ an integral homology isomorphism, while the definition of weak equivalence makes it an isomorphism on all based homotopy groups and a bijection on components. Thus $Z$ is path connected and simply connected, and the inclusion $j : X \to Z$ has precisely the required homology hypotheses, since $Q_{*} j_{*} = f_{*}$ .

2.1step 1.1F2F3F4∎

Apply the preceding lemma to $j$ and compose with $Q_{*}$ . This avoids assuming that an ordinary finite product of arbitrary CW complexes has its naive product topology as a CW topology. No lift of $f$ through an unrelated CW approximation is asserted.

Depends on

Used by

The finite Thom detector is a homotopy isomorphism through 2r−2 Theorem

Dependency tree · two levels

32 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, Chapter 4 (standard reference, not scraped)