Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-10
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.

Mapping cylinder factorization

Statement

For a continuous map f:X→Y of CGWH spaces, f=rj through its mapping cylinder, j is an unbased cofibration, and the included Y is a strong deformation retract of Mf. The construction is natural for strictly commuting squares. The corresponding based constructions hold for reduced mapping cylinders; the based inclusion X→CX at the base of the reduced cone is a based cofibration.

Facts & Assumptions

[F1]

The cylinder identifies (x,0) with f(x) and its free end is j(x)=[x,1]. Mapping cylinder and mapping cone

[F2]

The cylinder and closed-end quotient constructions are CGWH. Compact generation preserves the cylinder and closed pushouts

[F3]

Products of quotient maps with I are quotient. Interval exponential law and quotient homotopies

[F5]

A strong deformation retract keeps the retracted subspace fixed throughout the deformation. Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise

Proof

Given: The spaces, maps, and hypotheses in the statement above.

1.1F1F2F3F5

F2 makes the cylinder CGWH and its free end a closed embedded copy of X. By the defining formulas, rj(x)=f(x). Define D(y,t)=y and D([x,s],t)=[x,(1−t)s]. At s=0 both clauses have value f(x); F3 makes the induced homotopy continuous. It starts at the identity, ends at the inclusion followed by r, and fixes Y at every time. This is the claimed strong deformation retraction by F5.

1.2F1F4

Given initial data a:Mf→Z and a homotopy b:X×I→Z with b(x,0)=a(j(x)), prescribe data on the bottom and two vertical sides of the square with coordinates (s,t): a([x,s]) on t=0, b(x,t) on s=1, and a(f(x)) on s=0. The corner values agree. Keep a(y) constant on Y. Put λ=1/max⁡(1−t/2,2∣s−1/2∣) and R(s,t)=(1/2+λ(s−1/2),2+λ(t−2)). The denominator is at least 1/2. If its first term is maximal the second output is zero; otherwise the first output is 0 or 1. Both coordinates lie in I, and on the three designated sides λ=1. Thus R is a continuous retraction onto those sides.

2.1F1F3F4step 1.2

Compose the pasted side data with R. This gives a continuous extension on X×I×I; its value at s=0 is always a(f(x)). Together with the constant homotopy on Y, F3 descends it to Mf×I. It restricts to a initially and to b on the free end, proving HEP. If a commuting square is vf=f′u, the map [x,s]↦[u(x),s], y↦v(y) respects the attaching relation and all displayed height formulas. This proves naturality of the factorization and deformation.

3.1F2F3step 1.2step 2.1∎

For based data the values on the basepoint track are constant, so the same formulas descend after collapsing that track. Interchange the two vertical sides in step 1.2 to extend a prescribed homotopy at the base s=0 of the reduced cone, keeping the tip s=1 constant. Descent then proves the based cone-base cofibration as well. Empty X gives the unchanged space Y and an empty free-end inclusion.

Depends on

Dependency tree · 2 levels

Sources