Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passverified 2026-09-10 (Codex)
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 (X,A) is a relative CW complex, then A↪X has the homotopy extension property; in particular it is a cofibration.

Explicitly, for every topological space Y, continuous g:X→Y, and continuous H:A×I→Y satisfying H(a,0)=g(a), there is a continuous H~:X×I→Y restricting to H on A×I and to g at time zero. Here I=[0,1] and products have their ordinary product topologies. There is no finiteness or dimension bound on the CW complex, no separation hypothesis on Y, and no choice assumption. The CW structure, including its characteristic maps, is supplied as data.

Facts & Assumptions

Given: A map g:X→Y and a homotopy H:A×I→Y with H(a,0)=g(a).

[L1]

The skeleta Xn are obtained by attachment quotients, X is Hausdorff with the weak topology on its closed cells, and A 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).

[L3]

Write P=C(I,Y) with the compact-open topology. For every topological space Z, a function h:Z×I→Y is continuous exactly when its transpose h^:Z→P, h^(z)(t)=h(z,t), is well defined and continuous. This is the published exponential law, with metric domain I, after interchanging the product coordinates (The compact-open topology on C(X,Y) for a metric domain X, with subbasis S(K,V)={f:f[K]⊆V}, The exponential law: for a locally compact metric X and any spaces Z and Y, transposition is a bijection between C(X×Z,Y) and C(Z,C(X,Y)) with the compact-open topology).

[L4]

For a quotient map q:E→B, a subset of B is open, or closed, exactly when its inverse image under q 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).

[L6]

A specified successor operation can be iterated on the natural numbers without any choice principle (The recursion theorem).

Proof

technique · direct
1.1L3L4

First establish the needed quotient-cylinder mapping criterion. Let q:E→B be any quotient map and let h:B×I→Y be a function such that h∘(q×idI) is continuous. For each b, surjectivity supplies a representative e and shows that the path t↦h(b,t) is continuous. No simultaneous selection of representatives is needed. The continuous transpose upstairs is h^∘q:E→P. For every open V⊆P, its inverse image is q−1[h^−1[V]], so the quotient criterion makes h^−1[V] open. Thus h^ and then h are continuous. No closedness hypothesis on q is used.

1.2L5algebraconstruct

For n≥1, put Tn=(Dn×{0})∪(Sn−1×I). For u∈Dn and t∈I, define a=max⁡{1−t/2,∥u∥}, λ=1/a, and rn(u,t)=(λu,2+λ(t−2)). Since 1/2≤a≤1, this formula is continuous and defined on the entire cylinder. Moreover 1≤λ≤2/(2−t), so its height lies in [0,t], and λ∥u∥≤1. If a=1−t/2 the height is zero, while if a=∥u∥ the norm of the first coordinate is one; hence the image lies in Tn. If t=0 or ∥u∥=1, then a=1 and the point is fixed. Thus rn is a retraction onto Tn. For n=0 set r0(∗,t)=(∗,0).

1.3givenL1construct

We specify compatible continuous maps Hn:Xn×I→Y, with Hn(x,0)=g(x) and Hn=H on (A∩Xn)×I. On the discrete zero skeleton prescribe H0(v,t)=H(v,t) for v∈A and H0(v,t)=g(v) otherwise. Every vertex cylinder is open, so this is continuous.

1.4L1L2L4L5

We justify the infinite-stage continuity using the weak topology on X, not an assumed weak topology on X×I. Each characteristic map ϕ:Dn→e‾ is a quotient map. Indeed it is a continuous surjection; if F⊆Dn is closed, it is compact. Its image is compact by pulling any open cover of ϕ[F] back to F and retaining the images' finitely many covering members. This open-cover argument works for arbitrary targets, without a metrizability hypothesis on e‾. Since e‾ is a subspace of the Hausdorff space X, ϕ[F] is closed there. Thus ϕ is closed; if ϕ−1[C] is closed, then C=ϕ[ϕ−1[C]] is closed, proving the quotient criterion.

2.1givenL1L4step 1.2step 1.3

Given such Hn−1 for n≥1, let ϕα:Dn→Xn be a supplied characteristic map and fα:Sn−1→Xn−1 its boundary map. If its open cell belongs to A, use Kα(u,t)=H(ϕα(u),t); this is defined on the whole disk cylinder because the closed cell lies in A. For every other cell define bα:Tn→Y by bα(u,0)=g(ϕα(u)) and bα(u,t)=Hn−1(fα(u),t) for u∈Sn−1. These two continuous prescriptions agree on the corner and their domains form a two-piece closed cover of Tn, so bα is continuous. Set Kα=bα∘rn.

3.1L1step 1.1step 2.1

The maps Hn−1 and all Kα agree on the attaching identifications, including for cells belonging to A, and so determine a function Hn:Xn×I→Y. The map from (Xn−1⊔∐αDn)×I is continuous: each summand cylinder is open and carries the prescribed continuous map. The attachment map Xn−1⊔∐αDn→Xn is quotient, so step 1.1 proves continuity of Hn. Its time-zero values are g, it extends Hn−1, and it equals H on (A∩Xn)×I, since every cell of this intersection is either in the previous skeleton or among the cells on which Kα was prescribed from H.

4.1L6step 1.3step 3.1

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 Hn. The state space can be taken to be the set of valid stage-number/partial-map pairs, with the successor just constructed. Define H~(x,t)=Hn(x,t) whenever x∈Xn. Compatibility makes this independent of n, gives H~(x,0)=g(x), and gives H~∣A×I=H.

5.1L1L3L4step 4.1step 1.4

Every path t↦H~(x,t) is continuous by some Hn, so the transpose G:X→P is well defined. For each characteristic map ϕ:Dn→X, the map H~∘(ϕ×idI) is continuous by construction, and [L3] makes G∘ϕ continuous. By the quotient property from step 1.4, G∣e‾ is continuous. Consequently, for every closed C⊆P, the set G−1[C] meets every closed cell in a relatively closed set. The CW weak topology implies G−1[C] is closed in X. Thus G is continuous. This argument permits arbitrary families of cells and unbounded dimension.

6.1L3step 4.1step 5.1∎

The exponential law applied once more, now to G:X→P, proves that H~:X×I→Y 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

Used by

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