The source of a map is a cofibration in its mapping cylinder

The bottom face of the mapping cylinder of f : C(X, Y) has the homotopy extension property inside the mapping cylinder, so TauCeti.MappingCylinder.incl is a closed cofibration. Together with TauCeti.MappingCylinder.proj_comp_incl and TauCeti.MappingCylinder.homotopyEquiv this factors an arbitrary continuous map as a closed cofibration followed by a homotopy equivalence.

The retraction proving the property is assembled from a single retraction of the square I × I, in which the first coordinate is the height in the cylinder and the second is the time of the homotopy: the square is projected from the point (1, 2) onto the union of the side {0} × I with the bottom I × {0}. Projecting from a point on the line of height 1 is what makes the retraction compatible with the gluing, since it keeps the whole top face at height 1 and merely resets its time to 0, which is how the base of the mapping cylinder must move. It is this last property that an abstract retraction, such as the one behind TauCeti.hasHomotopyExtensionProperty_sphere_closedBall, does not supply, so the square retraction is written out.

Main results

• TauCeti.MappingCylinder.hasHomotopyExtensionProperty_range_incl: the source of f is a closed cofibration in the mapping cylinder of f.

References

• A. Hatcher, Algebraic Topology, Chapter 0, the section "The Homotopy Extension Property", where the mapping cylinder is used to replace a map by a cofibration.
• G. W. Whitehead, Elements of Homotopy Theory, Chapter I.

theorem TauCeti.MappingCylinder.hasHomotopyExtensionProperty_range_incl {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] {f : C(X, Y)} : HasHomotopyExtensionProperty (Set.range ⇑(incl f))

The source of f is a closed cofibration in the mapping cylinder of f: the bottom face of the cylinder has the homotopy extension property inside the mapping cylinder.