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.
Relative CW inclusions are cofibrations
Statement
If is a relative CW complex, then has the homotopy extension property; in particular it is a cofibration.
Explicitly, for every topological space , continuous , and continuous satisfying , there is a continuous restricting to on and to at time zero. Here and products have their ordinary product topologies. There is no finiteness or dimension bound on the CW complex, no separation hypothesis on , and no choice assumption. The CW structure, including its characteristic maps, is supplied as data.
Facts & Assumptions
Given: A map and a homotopy with .
The skeleta are obtained by attachment quotients, is Hausdorff with the weak topology on its closed cells, and is a union of cells containing the closure of each of its cells (Skeleta, CW subcomplexes, and relative CW complexes, CW complex with closure finiteness and weak topology, Cell attachment by a characteristic map).
The interval and the closed disks are compact: use Heine–Borel and the agreement of metric and topological compactness; is a singleton. In particular is a locally compact metric space (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, 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, Locally compact metric space: every point has a compact neighbourhood).
Write with the compact-open topology. For every topological space , a function is continuous exactly when its transpose , , is well defined and continuous. This is the published exponential law, with metric domain , after interchanging the product coordinates (The compact-open topology on for a metric domain , with subbasis , The exponential law: for a locally compact metric and any spaces and , transposition is a bijection between and with the compact-open topology).
For a quotient map , a subset of is open, or closed, exactly when its inverse image under is so (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection). Composites are continuous and continuous maps paste on a finite closed cover (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).
Closed subspaces of compact spaces are compact, and compact subsets of a Hausdorff space are closed (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact, 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). The Euclidean norm is continuous (The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for ).
A specified successor operation can be iterated on the natural numbers without any choice principle (The recursion theorem).
Proof
First establish the needed quotient-cylinder mapping criterion. Let be any quotient map and let be a function such that is continuous. For each , surjectivity supplies a representative and shows that the path is continuous. No simultaneous selection of representatives is needed. The continuous transpose upstairs is . For every open , its inverse image is , so the quotient criterion makes open. Thus and then are continuous. No closedness hypothesis on is used.
For , put . For and , define , , and . Since , this formula is continuous and defined on the entire cylinder. Moreover , so its height lies in , and . If the height is zero, while if the norm of the first coordinate is one; hence the image lies in . If or , then and the point is fixed. Thus is a retraction onto . For set .
We specify compatible continuous maps , with and on . On the discrete zero skeleton prescribe for and otherwise. Every vertex cylinder is open, so this is continuous.
We justify the infinite-stage continuity using the weak topology on , not an assumed weak topology on . Each characteristic map is a quotient map. Indeed it is a continuous surjection; if is closed, it is compact. Its image is compact by pulling any open cover of back to and retaining the images' finitely many covering members. This open-cover argument works for arbitrary targets, without a metrizability hypothesis on . Since is a subspace of the Hausdorff space , is closed there. Thus is closed; if is closed, then is closed, proving the quotient criterion.
Given such for , let be a supplied characteristic map and its boundary map. If its open cell belongs to , use ; this is defined on the whole disk cylinder because the closed cell lies in . For every other cell define by and for . These two continuous prescriptions agree on the corner and their domains form a two-piece closed cover of , so is continuous. Set .
The maps and all agree on the attaching identifications, including for cells belonging to , and so determine a function . The map from is continuous: each summand cylinder is open and carries the prescribed continuous map. The attachment map is quotient, so step 1.1 proves continuity of . Its time-zero values are , it extends , and it equals on , since every cell of this intersection is either in the previous skeleton or among the cells on which was prescribed from .
These formulas define the successor map uniquely from the preceding stage; they do not choose one extension from a nonempty set of extensions. Apply ordinary recursion, recording the stage number together with the partial map, to obtain all . The state space can be taken to be the set of valid stage-number/partial-map pairs, with the successor just constructed. Define whenever . Compatibility makes this independent of , gives , and gives .
Every path is continuous by some , so the transpose is well defined. For each characteristic map , the map is continuous by construction, and [L3] makes continuous. By the quotient property from step 1.4, is continuous. Consequently, for every closed , the set meets every closed cell in a relatively closed set. The CW weak topology implies is closed in . Thus is continuous. This argument permits arbitrary families of cells and unbounded dimension.
The exponential law applied once more, now to , proves that is continuous. Its restrictions established in step 4.1 solve every homotopy-extension problem in the statement, which is the asserted cofibration property.
Depends on
- Skeleta, CW subcomplexes, and relative CW complexes
- CW complex with closure finiteness and weak topology
- Cell attachment by a characteristic map
- The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection
- The exponential law: for a locally compact metric $X$ and any spaces $Z$ and $Y$, transposition is a bijection between $C(X \times Z, Y)$ and $C(Z, C(X,Y))$ with the compact-open topology
- The compact-open topology on $C(X,Y)$ for a metric domain $X$, with subbasis $S(K,V) = \{f : f[K] \subseteq V\}$
- Locally compact metric space: every point has a compact neighbourhood
- 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
- A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact
- 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
- Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous
- The finite and reverse triangle inequalities for a norm; and for $n \ge 1$ every norm $N$ on $\mathbb{R}^n$ satisfies $N(x) \le C\lVert x\rVert_1$ and is Lipschitz, hence continuous, for $d_2$
- The recursion theorem
Used by
- Elementary expansions and collapses of finite CW complexes Definition
- The Thom prespectrum of the universal real and oriented bundles Definition
- Complex K-AHSS for complex projective space Example
- A handle decomposition gives a relative CW complex Lemma
- A lifted finite CW equivalence has a contractible group-ring mapping cone Lemma
- A relative single cell layer has compatible homotopy and homology bases Lemma
- An identity relative homotopy matrix permits cell cancellation Lemma
- Attaching a single cell kills the represented homotopy class Lemma
- Based loop spaces of CW complexes have CW homotopy type Lemma
- Cell slides and stabilizations realize elementary group-ring matrices Lemma
- Cell trading puts a finite relative equivalence in two high degrees Lemma
- Cw homotopy equivalence inclusions are strong deformation retracts Lemma
- CW quotients and collapse of a contractible subcomplex Lemma
- Finite relative homotopy lifting across a weak equivalence Lemma
- Homological AHSS exact couple from the skeletal filtration Lemma
- Iterated suspension and winding control Lemma
- Local path-fibration and cohomology inputs for mod-two Eilenberg–Mac Lane induction Lemma
- p-surgery kills the represented pi-p class below the middle dimension Lemma
- Relative Morse–Bott crossing by negative normal disk bundles Lemma
- Relative singular product comparison for CW pairs Lemma
- Serre-fibration replacement preserves fiber homology transport Lemma
- Suspension, exactness, and products in relative KO Lemma
- The AHSS E-one page is cellular cochains with theory coefficients Lemma
- The AHSS first differential is the cellular coboundary Lemma
- The graded Chern character respects relative maps and skeletal filtrations Lemma
- The skeletal telescope projects by a homotopy equivalence of pairs Lemma
- Vanishing relative homotopy extends an inverse over cells Lemma
- Weak equivalences of pairs induce isomorphisms on relative homotopy Lemma
- Weak homotopy equivalences induce integral homology isomorphisms without choice Lemma
- Reduced and unreduced generalized cohomology theories correspond Proposition
- Surgery on a normal map preserves its normal bordism class Proposition
- The first Stiefel–Whitney class classifies orientability Proposition
- Unreduced pair and reduced quotient axioms are equivalent on cw pairs Proposition
- Affine Clifford–Hopf maps are highly connected Theorem
- Cellular approximation for maps of CW pairs Theorem
- Cohomological Serre spectral sequence Theorem
- Homological Atiyah–Hirzebruch spectral sequence Theorem
- Singular homology satisfies homotopy exactness and excision Theorem
- Smale–Hirsch for open source manifolds Theorem
- The first Chern class classifies complex line bundles Theorem
Dependency tree · two levels
80 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, Proposition 0.16 (standard reference, not scraped)