Products of closed cofibrations

If closed subsets A ⊆ X and B ⊆ Y have the homotopy extension property, then so does A × Y ∪ X × B ⊆ X × Y (Strøm's product theorem). No compactness or separation hypothesis is needed. The proof passes through NDR data: closed cofibrations are exactly the subsets admitting NDR data (TauCeti.nonempty_ndrPair_iff), and NDR pairs have products (TauCeti.NDRPair.prod). Both subsets are assumed closed here, as NDR data requires; Strøm's theorem needs only one of them closed.

Two special cases are recorded.

• Taking B = ∅, the product Y × A ⊆ Y × X of a closed cofibration with any space is a cofibration. This allows homotopies to be extended continuously in additional parameters, in particular when proving the homotopy lifting property of restriction between compact-open mapping spaces.
• Taking {0, 1} ⊆ I as the first factor, {0, 1} × X ∪ I × A ⊆ I × X is a cofibration: a homotopy of maps out of X × I may be prescribed at both ends and over A at once. This is the form in which homotopies between homotopies are extended, as in the proof that a homotopy equivalence between cofibrations under A is a homotopy equivalence relative to A.

Main declarations

• TauCeti.HasHomotopyExtensionProperty.prod_univ_union_univ_prod: Strøm's product theorem for closed cofibrations.
• TauCeti.HasHomotopyExtensionProperty.univ_prod: products with arbitrary spaces.
• TauCeti.HasHomotopyExtensionProperty.zero_one_prod_univ_union_univ_prod: the cylinder on a closed cofibration, relative to both of its ends.

References

• A. Strøm, Note on cofibrations II, Math. Scand. 22 (1968), 130–142, for the product theorem.
• A. Hatcher, Algebraic Topology, Chapter 0, Proposition 0.19, where the cylinder case is used.
• G. W. Whitehead, Elements of Homotopy Theory, Chapter I, homotopy extension and cofibrations.

theorem TauCeti.HasHomotopyExtensionProperty.prod_univ_union_univ_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {A : Set X} {B : Set Y} (hA : HasHomotopyExtensionProperty A) (hA' : IsClosed A) (hB : HasHomotopyExtensionProperty B) (hB' : IsClosed B) : HasHomotopyExtensionProperty (A ×ˢ Set.univ ∪ Set.univ ×ˢ B)

Strøm's product theorem: if closed subsets A ⊆ X and B ⊆ Y have the homotopy extension property, then so does A × Y ∪ X × B ⊆ X × Y.

theorem TauCeti.HasHomotopyExtensionProperty.univ_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {A : Set X} (h : HasHomotopyExtensionProperty A) (hA : IsClosed A) : HasHomotopyExtensionProperty (Set.univ ×ˢ A)

A closed cofibration remains a cofibration after taking its product with any space.

theorem TauCeti.HasHomotopyExtensionProperty.zero_one_prod_univ_union_univ_prod {X : Type u_1} [TopologicalSpace X] {A : Set X} (h : HasHomotopyExtensionProperty A) (hA : IsClosed A) : HasHomotopyExtensionProperty ({0, 1} ×ˢ Set.univ ∪ Set.univ ×ˢ A)

The cylinder on a closed cofibration: if a closed subset A ⊆ X has the homotopy extension property, then so does {0, 1} × X ∪ I × A ⊆ I × X.