Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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 X, write π0(X) for its set of path components, as defined in Paths, path-connected spaces and path components. For xX and n1, use the based cubical homotopy group πn(X,x) 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 f:XY is a weak homotopy equivalence when both of the following hold:

  • The function π0(f):π0(X)π0(Y) is bijective.
  • For every xX and every integer n1, the homomorphism f:πn(X,x)πn(Y,f(x)) 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

[F1]

Higher homotopy group by based cubes defines the based homotopy sets used here.

[F2]

Paths, path-connected spaces and path components defines the equivalence classes of points under paths.

[F3]

Higher homotopy groups are functorial and based homotopy invariant supplies the well-defined induced homomorphisms.

Verification

Given: A continuous map f:XY and the two conditions in the definition.

1.1

Paths in X are sent to paths in Y by continuous composition, so the function on the equivalence classes defining π0 is well defined. For positive degrees [F3] proves that postcomposition on the based cubes of [F1] is a well-defined homomorphism, with boundary value f(x). Thus both conditions refer to already-defined maps, for every actual source point; no representative from each component is selected.

F1F2F3
2.1

If X is empty, its component set is empty. A nonempty Y has a point y and hence the nonempty component containing y, so component bijectivity forces Y 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.

F2F3

Depends on

Used by

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