Local-to-global homotopy lifting over numerable covers

Dold's local-to-global theorem for fibrations: let p : E → B be a continuous map and (U i)_{i ∈ ι} a numerable cover of B, meaning there exists a locally finite partition of unity ρ : PartitionOfUnity ι B with support (ρ i) ⊆ U i for all i. If for a space A each restriction p ⁻¹' U i → U i has the homotopy lifting property with respect to every open subset of A, then p has the homotopy lifting property globally with respect to A (TauCeti.HasHomotopyLiftingProperty.of_partitionOfUnity).

In particular, if each restriction p ⁻¹' U i → U i is a Hurewicz fibration, then p is a Hurewicz fibration (TauCeti.isHurewiczFibration_of_partitionOfUnity), with no separation, countability or paracompactness assumption on the test spaces. Over a normal paracompact base (which includes every paracompact Hausdorff base via Mathlib's NormalSpace instance), any open cover is numerable, so a map that is locally a Hurewicz fibration over an open cover is globally a Hurewicz fibration (TauCeti.isHurewiczFibration_of_isOpenCover).

Implementation notes

Given a homotopy H : C(I × A, B) starting at p ∘ f on a nonempty space A:

1. For each subdivision number m + 1 and tuple α : Fin (m + 1) → ι, define the tube weight η m α a = ⨅ k, ⨅ t ∈ [k/(m+1), (k+1)/(m+1)], ρ (α k) (H (t, a)). Compactness of the segments makes η m α continuous, and the Lebesgue number lemma on I supplies a positive weight at each a : A.
2. Truncating η m α a by (m : ℝ) * ∑_{j < m} sup_β η j β a produces a single locally finite nonnegative family positive at every point of A, normalized via PartitionOfUnity.ofExistsPos to a partition of unity ν on A.
3. Applying PartitionOfUnity.gapPartition and PartitionOfUnity.shrink yields a countable partition of unity μ : PartitionOfUnity ℕ A whose n-th closed support lies inside the union of the pairwise disjoint open gap strata {a | 0 < ν.gap E a} with #E = n.
4. Stepping along the cumulative sums τ n a = ∑_{j < n} μ j a lifts H up to time τ n by finitely many local lifts on each gap stratum; local finiteness of μ makes the sequence of partial lifts locally stationary near every point of A.

Main results

• TauCeti.HasHomotopyLiftingProperty.of_partitionOfUnity: Dold's local-to-global homotopy lifting theorem over a numerable cover.
• TauCeti.HasHomotopyLiftingProperty.of_isOpenCover: local-to-global homotopy lifting over an open cover of a normal paracompact base.
• TauCeti.isHurewiczFibration_of_partitionOfUnity: a continuous map locally a Hurewicz fibration over a numerable cover is a Hurewicz fibration.
• TauCeti.isHurewiczFibration_of_isSubordinate: convenience form for closed-support subordination ρ.IsSubordinate U.
• TauCeti.isHurewiczFibration_of_isOpenCover: a continuous map locally a Hurewicz fibration over an open cover of a normal paracompact base is a Hurewicz fibration.

References

• A. Dold, Partitions of unity in the theory of fibrations, Ann. of Math. (2) 78 (1963), 223–255, Theorem 4.8.
• A. Hatcher, Algebraic Topology, Theorem 4.42.

theorem TauCeti.HasHomotopyLiftingProperty.of_partitionOfUnity {ι : Type u_1} {E : Type u} {B : Type v} {A : Type w} [TopologicalSpace E] [TopologicalSpace B] [TopologicalSpace A] {p : E → B} {U : ι → Set B} (ρ : PartitionOfUnity ι B) (hρ : ∀ (i : ι), Function.support ⇑(ρ i) ⊆ U i) (hlift : ∀ (i : ι) (W : Set A), IsOpen W → HasHomotopyLiftingProperty (Set.MapsTo.restrict p (p ⁻¹' U i) (U i) ⋯) ↑W) : HasHomotopyLiftingProperty p A

Dold's local-to-global homotopy lifting theorem. Let p : E → B be a map and (U i)_{i ∈ ι} a numerable cover of B, witnessed by a partition of unity ρ : PartitionOfUnity ι B with support (ρ i) ⊆ U i for every i. If each restriction p ⁻¹' U i → U i has the homotopy lifting property with respect to every open subset of A, then p has the homotopy lifting property with respect to A.

theorem TauCeti.HasHomotopyLiftingProperty.of_isOpenCover {ι : Type u_1} {E : Type u} {B : Type v} {A : Type w} [TopologicalSpace E] [TopologicalSpace B] [TopologicalSpace A] [NormalSpace B] [ParacompactSpace B] {p : E → B} {U : ι → Set B} (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ∀ (b : B), ∃ (i : ι), b ∈ U i) (hlift : ∀ (i : ι) (W : Set A), IsOpen W → HasHomotopyLiftingProperty (Set.MapsTo.restrict p (p ⁻¹' U i) (U i) ⋯) ↑W) : HasHomotopyLiftingProperty p A

Over a normal paracompact base, a map whose restrictions to the members of an open cover have the homotopy lifting property with respect to every open subset of A has the homotopy lifting property globally with respect to A.

theorem TauCeti.isHurewiczFibration_of_partitionOfUnity {ι : Type u_1} {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : Continuous p) {U : ι → Set B} (ρ : PartitionOfUnity ι B) (hρ : ∀ (i : ι), Function.support ⇑(ρ i) ⊆ U i) (hpU : ∀ (i : ι), IsHurewiczFibration (Set.MapsTo.restrict p (p ⁻¹' U i) (U i) ⋯)) : IsHurewiczFibration p

Dold's local-to-global theorem for Hurewicz fibrations. A continuous map p : E → B whose restrictions p ⁻¹' U i → U i over a numerable cover (U i)_{i ∈ ι} of B (witnessed by a partition of unity ρ with support (ρ i) ⊆ U i) are Hurewicz fibrations is itself a Hurewicz fibration.

theorem TauCeti.isHurewiczFibration_of_isSubordinate {ι : Type u_1} {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : Continuous p) {U : ι → Set B} {ρ : PartitionOfUnity ι B} (hρ : ρ.IsSubordinate U) (hpU : ∀ (i : ι), IsHurewiczFibration (Set.MapsTo.restrict p (p ⁻¹' U i) (U i) ⋯)) : IsHurewiczFibration p

Convenience form of TauCeti.isHurewiczFibration_of_partitionOfUnity for a partition of unity subordinate to U in the closed-support sense (PartitionOfUnity.IsSubordinate).

theorem TauCeti.isHurewiczFibration_of_isOpenCover {ι : Type u_1} {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] [NormalSpace B] [ParacompactSpace B] {p : E → B} (hp : Continuous p) {U : ι → Set B} (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ∀ (b : B), ∃ (i : ι), b ∈ U i) (hpU : ∀ (i : ι), IsHurewiczFibration (Set.MapsTo.restrict p (p ⁻¹' U i) (U i) ⋯)) : IsHurewiczFibration p

Over a normal paracompact base (including every paracompact Hausdorff base), a continuous map that is locally a Hurewicz fibration over an open cover is globally a Hurewicz fibration.