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.
Each homotopy representative is supported on a finite CW subcomplex
Statement
For a CW complex , every continuous map from a compact sphere or disk into has image in a finite CW subcomplex. Every specified homotopy between such maps also has image in a finite CW subcomplex. These assertions quantify separately over each map and each homotopy; they do not assert a single finite subcomplex that works for all representatives.
If the chosen basepoint is a zero-cell, every based homotopy class in , , has a representative whose image is contained in . No such based skeletal assertion is made for a basepoint outside . All these conclusions are choice-free: only the finite-relative-source clause of cellular approximation is used.
Facts & Assumptions
Compact CW images have finite cell support without choice puts every compact-source image in a finite target subcomplex, without choice.
Cellular approximation for maps of CW pairs gives a homotopy rel a subcomplex to a cellular map without choice when there are finitely many relative source cells.
Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line and For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide give compactness of closed bounded Euclidean subsets in the topological sense.
In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones and A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact give the closedness and compactness used for the sphere quotient.
Proof
Given: A CW complex , one map or , or one specified homotopy with one of these domains. For the based assertion, and is a zero-cell.
The Euclidean sphere and disk are closed and bounded, as are their products with , regarded as subsets of a finite-dimensional Euclidean space. Thus [F3] makes them compact. is a singleton and consists of two points, which are compact by taking one covering member for each of finitely many points. Their products with are a single interval or two intervals, also closed bounded Euclidean subsets after the usual embeddings.
The sphere has a finite -dimensional CW structure with its designated basepoint as a vertex. One concrete construction for attaches one -disk to a point by collapsing its entire boundary. To identify the quotient with , send of norm to , and send zero to the north pole. This is continuous at zero since , is constant at the south pole on the boundary, and is a bijection from the interior to the complement of that pole. The induced continuous bijection from the compact quotient to the Hausdorff sphere is a homeomorphism: the quotient is compact by pulling open covers back to the disk. A closed subset is compact by [F4], its image is compact by the same cover argument, and that image in the Hausdorff sphere is closed by [F4]. Identify the pole with the designated sphere basepoint. This realizes the usual two-cell based sphere.
Apply [F1] directly to , and separately to the specified . It gives finite subcomplexes containing their images. The finite subcomplex for automatically contains both endpoint images, since the endpoints are restrictions of . This does not require selecting representatives of a family of homotopy classes, nor choosing simultaneous finite subcomplexes for such a family.
For a given based representative , its restriction to the source vertex is cellular because . Apply the finite-relative-source clause of [F2] to and . It produces a based homotopy to that is cellular. The source has dimension , so . Since the homotopy fixes the basepoint, represents precisely the original based class. This applies to each class by beginning with any one representative; it asserts existence for each class and does not select representatives simultaneously.
Each homotopy just obtained, being a specified map on , also satisfies step 2.1. A basepoint outside cannot belong to the image of a based map landing in , so such a skeletal conclusion would be impossible and has not been asserted. The assertions about compact images have no basepoint restriction. Zero-dimensional compact domains were treated in step 1.1; the skeletal group assertion begins at , and no group law is implied. Only choice-free [F1], [F3] and the expressly choice-free clause of [F2] have been used.
Depends on
- Cellular approximation for maps of CW pairs
- Compact CW images have finite cell support without choice
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide
- In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones
- A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
48 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 Appendix A and Theorem 4.8 (standard reference, not scraped)