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.
Weak homotopy equivalence
Definition
For a topological space , write for its set of path components, as defined in Paths, path-connected spaces and path components. For and , use the based cubical homotopy group of Higher homotopy group by based cubes. Postcomposition gives the maps on components and the homomorphisms on based groups by Higher homotopy groups are functorial and based homotopy invariant.
A continuous map is a weak homotopy equivalence when both of the following hold:
- The function is bijective.
- For every and every integer , the homomorphism is an isomorphism.
The quantifiers include every component and every source basepoint; no representative point is chosen in each component. Degree zero is a condition on sets, not on groups. Degree one uses the possibly nonabelian fundamental group. The definition applies to arbitrary spaces without separation or CW hypotheses and uses no choice principle.
For the empty source the second condition is vacuous, but the first forces the target to be empty: every point of a nonempty target belongs to a path component. Thus the unique empty-to-empty map is a weak homotopy equivalence, whereas an empty-to-nonempty map is not. The identity of any space, including a singleton, satisfies both conditions since its induced maps are identities.
Facts & Assumptions
Higher homotopy group by based cubes defines the based homotopy sets used here.
Paths, path-connected spaces and path components defines the equivalence classes of points under paths.
Higher homotopy groups are functorial and based homotopy invariant supplies the well-defined induced homomorphisms.
Verification
Given: A continuous map and the two conditions in the definition.
Paths in are sent to paths in by continuous composition, so the function on the equivalence classes defining is well defined. For positive degrees [F3] proves that postcomposition on the based cubes of [F1] is a well-defined homomorphism, with boundary value . Thus both conditions refer to already-defined maps, for every actual source point; no representative from each component is selected.
If is empty, its component set is empty. A nonempty has a point and hence the nonempty component containing , so component bijectivity forces empty. If both spaces are empty, component bijectivity holds and all pointwise conditions are vacuous. For an identity map on any space, [F3] gives identity induced maps on components and all positive groups, so the two conditions hold, including for a singleton. These checks use no choice and do not replace the condition in degree zero by a group assertion.
Depends on
Used by
- A weakly contractible CW complex is contractible Corollary
- Whitehead theorem fails without CW type Counterexample
- A simply connected CW homology equivalence is a homotopy equivalence under the stated choice conditions Example
- A connected CW pair has a model without low relative cells Lemma
- A weak equivalence has vanishing mapping-cylinder relative groups Lemma
- CW quotients and collapse of a contractible subcomplex Lemma
- Finite relative homotopy lifting across a weak equivalence Lemma
- Homotopy excision for a single relative cell layer Lemma
- Weak equivalences glue along a common connected CW subcomplex Lemma
- Weak equivalences of pairs induce isomorphisms on relative homotopy Lemma
- Whitehead theorem Theorem
Dependency tree · two levels
18 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
- Hatcher §4.1; May Chapter 10 §3 (standard reference, not scraped)