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.
A fibration has path lifting and homotopy lifting relative to a subspace
Statement
Both kinds of fibration lift every path with any prescribed initial point. For a Serre fibration, every homotopy on a CW complex lifts with a prescribed compatible lift on , where is a CW subcomplex. This unrestricted CW clause assumes AC; finite CW pairs require no AC. Thus disk tests and CW tests are equivalent under AC. A Hurewicz fibration in CGWH has the same relative property for every closed cofibration pair . This clause is choice-free. No assertion is made for arbitrary subspaces.
Facts & Assumptions
HLP specifies the initial map and the projection of the entire lift. Hurewicz and serre fibrations
A closed cofibration has continuous NDR data , with , , , and if ; these are derived in proof steps 1.2–2.1 of the supplier. Pushouts and products preserve the cofibrations used here
Compact-time tracks give uniform neighbourhood control. Tube lemma: if is compact and an open contains , then contains for some open
Transposition against preserves continuity, also with CG conventions. Interval exponential law and quotient homotopies
CW spaces have the weak topology determined by characteristic disks. CW complex with closure finiteness and weak topology
A subcomplex contains all boundaries of its cells. Skeleta, CW subcomplexes, and relative CW complexes
AC selects lifts in arbitrary sets of nonempty lifting problems. The Axiom of Choice
Proof
Given: A map of the indicated type and compatible continuous data , , where and .
Taking in F1 gives path lifting, including constant paths and any initial point that exists. If is empty the unique empty lift suffices. This does not assert that a lift of a constant path is constant.
Disk HLP also solves a disk-cylinder problem prescribed on its bottom and sides. Here is the geometric change of domain: is a boundary disk parametrized by for and for . This is a homeomorphism from , with boundary the top rim. The complementary top disk has the same boundary parametrization. Parametrize the two hemispheres of a sphere by these two disks; the resulting boundary homeomorphism extends radially from an interior point to a homeomorphism of balls. Applying this construction both to the cylinder with its bottom face and to the cylinder with its bottom-and-sides gives a homeomorphism of these pairs. Thus F1 transfers to the required partial domain. For there are no sides and no change is needed.
For the Hurewicz clause use F2 and put . For define and for set . Away from these are continuous formulas. At , F3 and give, for any neighbourhood of , a neighbourhood with ; the second coordinate changes by at most . Hence continuity holds across , even at . We have and . At , either and the height is zero, or , whence and . Thus is a retraction.
Induct over dimensions of the cells of outside . On each characteristic disk the already prescribed data are exactly bottom-and-sides data; step 1.2 extends them. They agree on attaching boundaries, so descend to each skeleton. AC in F7 selects the extensions for unrestricted cell families, including the successive dimensions; a finite CW pair requires only finitely many choices. Continuity on all of follows without assuming an ordinary infinite product/colimit interchange: transpose the constructed function to . Its restriction to every characteristic disk is continuous by F4; F5 makes the transpose continuous, and F4 uncurries it. The initial and subcomplex values are unchanged at every stage. Taking proves the CW-test implication; conversely every disk is a CW complex.
Put , whose zero set is , and define by when , and on . F3 applied to the fixed tracks proves continuity at ; elsewhere it is composition of continuous maps. In particular , , and for .
Apply ordinary HLP in the chosen category once, with parameter , initial map , and base homotopy . It supplies with and . Then is continuous, , and for . This proves the full prescribed relative lift. When , and the construction returns ; when it still applies and ordinary HLP already suffices. The only selections here are one NDR witness and one HLP witness, not an indexed family, so no AC is used. In particular no regular lifting function is assumed.
Depends on
- Hurewicz and serre fibrations
- Cofibration and homotopy extension property
- Pushouts and products preserve the cofibrations used here
- Tube lemma: if $K$ is compact and an open $N \subseteq X \times Z$ contains $K \times \{z_0\}$, then $N$ contains $K \times W$ for some open $W \ni z_0$
- Interval exponential law and quotient homotopies
- CW complex with closure finiteness and weak topology
- Skeleta, CW subcomplexes, and relative CW complexes
- The Axiom of Choice
Used by
Dependency tree · two levels
27 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
- May, A Concise Course in Algebraic Topology (standard reference, not scraped)
- Hatcher, Algebraic Topology (standard reference, not scraped)