Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-13
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.

Finite relative homotopy lifting across a weak equivalence

Statement

Let f:PY be a weak homotopy equivalence of arbitrary spaces, and let (K,L) be a CW pair with finitely many cells outside L. Given continuous maps u:LP, v:KY and a homotopy T:L×IY with T(l,0)=v(l) and T(l,1)=f(u(l)), there are a continuous map w:KP extending u and a homotopy J:vfw such that J(l,t)=T(l,λ(t)),λ(t)=min(4t,1). In particular, if fu=vL and T is constant in time, then fwv rel L. More generally J is stationary at every point of L at which T is stationary. No choice principle is required; L may have arbitrary size and dimension.

Facts & Assumptions

[F1]

Weak homotopy equivalence gives all-basepoint weak equivalence. A weak equivalence has vanishing mapping-cylinder relative groups supplies component bijectivity and relative triviality for its ordinary mapping-cylinder source inclusion. That item's proof also establishes the embedded endpoints, retraction and continuous height deformation for arbitrary spaces.

[F2]

Relative cubical disk model and compression compresses a null relative disk into the subspace while fixing its entire boundary, in every positive degree including one.

[F3]

Relative CW inclusions are cofibrations gives the choice-free HEP for every CW subcomplex, with arbitrary target.

[F4]

Skeleta, CW subcomplexes, and relative CW complexes gives the subcomplexes LKd and their attachment structure. Interval exponential law and quotient homotopies says that an attachment quotient remains quotient after product with I. Every natural-number-indexed list of nonempty sets has a choice function on its family of values permits finitely many witness selections without AC.

Proof

Given: The spaces and maps in the statement. Write M=Mf, with j:PM, k:YM and r:MY, so rj=f and rk=idY.

1.1

The ordinary cylinder formulas and embeddings in [F1] are valid without separation assumptions. On L×I define a homotopy starting at kvL by B(l,s)={kT(l,2s),0s1/2,[u(l),2s1],1/2s1. At s=1/2 the two values are kfu(l)=[u(l),0], so finite closed pasting gives continuity. At s=1, its value is ju(l). By [F3], extend B from L to a homotopy V:K×IM starting at kv. Put b=V(,1), so bL=ju. Projection by r on L gives the precise formula rB(l,s)=T(l,min(2s,1)).

F1F3given
2.1

We compress this b into j(P) rel L using only finitely many source-cell choices. Write Dd=LKd, with D1=L. Suppose a current map bd1:KM equals ju on L and takes Dd1 into j(P). For a relative d-cell, its characteristic disk followed by bd1 has boundary in j(P). If d1, mark a fixed boundary point and use its actual image j(p) as basepoint. The relative class is null by [F1], so [F2] gives a compression into j(P) fixing all boundary points. If d=0, the component-surjectivity of j in [F1] gives a path from the image of that vertex into j(P). There are only finitely many relative cells in this dimension, so [F4] supplies their finitely many compression witnesses.

F1F2F4step 1.1
3.1

Glue these disk homotopies to the stationary homotopy on Dd1. They agree on every attaching identification, because disk boundaries were fixed. By [F4], Dd is the quotient of Dd1 and the finitely many characteristic d-disks by their boundary identifications, and the product of this quotient with I is again quotient. The compatible continuous homotopies on those pieces therefore descend to a continuous homotopy on Dd×I, even with an infinite-dimensional L. Extend it to K by [F3] for (K,Dd). Its endpoint bd sends Dd into j(P) and retains ju on L. Starting from b1=b, perform these stages through the maximum dimension of the finite set of relative cells. The HEP is specified without choices, and the remaining witness selections are a finite sequence. Concatenation gives a continuous C:K×IM from b to a map into j(P), fixed on L. If there are no relative cells, take C constant. Its endpoint factors continuously through the embedded subspace j(P) by [F1]; denote the resulting map by w:KP. It satisfies wL=u.

F1F3F4step 1.1step 2.1
4.1

Concatenate V and C on the two half-intervals and compose with r: J(x,t)={rV(x,2t),0t1/2,rC(x,2t1),1/2t1. The seam is rb(x), the initial value is v(x) and the final value is fw(x). On L, step 1.1 gives J(l,t)=T(l,min(4t,1)) for the first half; on the second half C is constantly ju, and its projection is fu(l)=T(l,1). Hence the displayed formula holds for all t. In particular any stationary T track stays stationary, and strict commuting data yield the rel-L conclusion.

F1step 1.1step 3.1
5.1

If P is empty, weak equivalence forces Y empty. Existence of v then forces K and L empty, and the unique maps satisfy the result. Empty L otherwise imposes no boundary condition; zero relative cells give w=u and the same reparametrized T. A zero-cell uses a path, and a one-cell compression fixes its two possibly distinct endpoints by [F2]. No choice is made on all of L: its homotopy is prescribed as data, and only the finitely many cells outside it request witnesses. The formula in step 4.1 checks t=0,1/4,1/2,1, so the plateau in λ is intentional and no claim of extending the original time parametrization is made. This proves every assertion choice-free.

F1F2F4step 1.1step 3.1step 4.1

Depends on

Used by

Dependency tree · two levels

38 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