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.
CW quotients and collapse of a contractible subcomplex
Statement
Let be a CW pair with and supplied characteristic maps. The ordinary quotient is a CW complex, with one vertex replacing and one cell of the same dimension for every cell of .
If admits a contraction , , , then the quotient map is a homotopy equivalence and a weak homotopy equivalence. If for every , the constructed inverse and inverse homotopies are based at and . No choice principle is required; a contraction is one witness, not a family of selected contractions.
Facts & Assumptions
Cellular attachments with finite boundary support form a CW complex constructs CW spaces by supplied ascending-dimensional attachments with cellular finite-support boundaries, and gives the characteristic-disk map-out criterion. Skeleta, CW subcomplexes, and relative CW complexes specifies the relative cells and their boundaries.
Relative CW inclusions are cofibrations extends a prescribed homotopy from a CW subcomplex with arbitrary target, without choice.
For a quotient map , a map out of is continuous iff its composite with is; a continuous map on constant on the fibres of factors uniquely through ; and a composite of quotient maps is a quotient map gives descent through ordinary quotient maps. Interval exponential law and quotient homotopies makes their products with quotient, so compatible homotopies descend jointly.
Higher homotopy basepoint transport and moving homotopies gives for a homotopy from to with basepoint track . Its radial-shell formula is natural under postcomposition. Weak homotopy equivalence also requires component bijectivity.
Proof
Given: The CW pair, and, for the homotopy-equivalence assertions, the specified contraction of to .
Start with the discrete vertex set consisting of and the vertices of . For each positive dimension attach the characteristic disks of the corresponding cells of , composing their original boundary maps with the collapse already constructed on and the lower-dimensional cells. This composition is continuous by induction on dimension. The boundaries are cellular and have finite support: a closed cell of has finite support by its supplied CW structure, and collapsing its portion in replaces that portion by at most the one vertex . Thus [F1] gives a CW complex with precisely the asserted cells. Points of the open cells outside are not identified with one another or with , so its underlying set is exactly the set .
This CW topology is the ordinary quotient topology. A function is continuous for the ordinary quotient exactly when is continuous, by [F3]. By the characteristic-disk test [F1], the latter means continuity on each characteristic disk of . Disks belonging to map constantly to ; the other tests are precisely the characteristic disks used to construct . Hence the map-out tests agree for every target . Taking to be the two-point space with open sets , the characteristic map of a subset is continuous exactly when that subset is open. Therefore the two topologies agree. In particular is Hausdorff and CW with the displayed quotient characteristic maps; no separation of an arbitrary quotient was assumed in advance.
Extend , viewed in , by [F2] from the initial map to a homotopy with and . Thus is constant at on and factors continuously as for by [F3]. For every , the map is constant at on , since stays in . Consequently the jointly continuous map descends through to a continuous by [F3]. It starts at the identity and ends at : the endpoint equality follows after composition with the surjective . We have proved and , with the exact identity .
These homotopies make the induced component functions of and inverse, because each point is joined to its image under the corresponding composite. For positive degree at any , put and , a path from to . The track of at is . Define By [F4] applied to , . The radial-shell formula in [F4] gives , where the right-hand is based at . Thus by [F4] applied to . Hence is an isomorphism at every basepoint, proving weak equivalence without a based-contraction assumption.
If fixes , then by its prescribed restriction, , and already holds by construction. Thus both maps and homotopies are based as asserted. If , the quotient CW consists only of , and the same contraction gives the claimed equivalence. If is a singleton, the quotient identifies no distinct points and the identity contraction is available. Empty is excluded because the displayed collapse has a specified quotient vertex; no empty-set contraction is postulated. Zero-dimensional relative cells are retained as separate vertices, higher-dimensional cells retain their supplied attaching identifications, and no regularity of those maps was used. Only the one given contraction and the specified choice-free HEP construction enter steps 3.1–4.1. This proves all assertions without AC.
Depends on
- Cellular attachments with finite boundary support form a CW complex
- Skeleta, CW subcomplexes, and relative CW complexes
- Relative CW inclusions are cofibrations
- For a quotient map $q : X \to Y$, a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$; and a composite of quotient maps is a quotient map
- Interval exponential law and quotient homotopies
- Higher homotopy basepoint transport and moving homotopies
- Weak homotopy equivalence
Used by
- A CW quotient induces relative singular homology isomorphisms Lemma
- A relative single cell layer has compatible homotopy and homology bases Lemma
- Cellular reduction for a highly connected pair Lemma
- Relative homotopy compares with the CW quotient in the connectivity range Lemma
- Freudenthal suspension theorem Theorem
Dependency tree · two levels
35 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.