The Main Theorems🔗

Assembling the reduction with the geometric core proved in Parts II and III yields the two theorems of the benchmark — Theorem A and Theorem B of the statement chapter, stated in full and proved.

namespace Submission

open _root_.FamiliesOfMapsB01
open _root_.FamiliesOfMapsB01.Subdivision
open Set unitInterval Geometry
open scoped Topology

namespace FamiliesOfMapsB01

variable {k : ℕ} {ι X T : Type*}
  [TopologicalSpace X] [TopologicalSpace T]

Theorem A (the continuous case):

/-- **Lemma B.0.1** of Morrison–Walker, *The Blob Complex*
(arXiv:1009.5025, §B), continuous case. -/
theorem continuous
    {P : Set (Fin k → ℝ)} (_hP : IsPolyhedron P)
    [CompactSpace X]
    (U : ι → Set X) (_hUopen : ∀ α, IsOpen (U α))
    (ρ : PartitionOfUnity ι X univ) (_hρ : ρ.IsSubordinate U)
    (f : C(P × X, T)) :
    ∃ F : C(I × P × X, T),
      (∀ p : P, ∀ x : X, F (0, p, x) = f (p, x)) ∧
      (∃ K : Subdivision P,
         ∀ D ∈ K.complex.facets,
            AdaptedTo U k
              (fun q : closedCell P D × X => F (1, q.1.1, q.2))) ∧
      (∀ S : Set X, Supported (f := f.toFun) S →
          Supported (fun q : (I × P) × X => F (q.1.1, q.1.2, q.2)) S) ∧
      (∀ Q : Set P, IsBoundarySubpolyhedron Q →
        ∀ S' : Set X,
          Supported (fun q : Q × X => f (q.1.1, q.2)) S' →
            Supported (fun q : (I × Q) × X => F (q.1.1, q.1.2.1, q.2)) S') := byk:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)_hP:IsPolyhedron Pinst✝:CompactSpace XU:ι → Set X_hUopen:∀ (α : ι), IsOpen[inst✝²] (U α)ρ:PartitionOfUnity ι X_hρ:ρ.IsSubordinate Uf:C(↑P × X, T)⊢ ∃ F,
  (∀ (p : ↑P) (x : X), F (0, p, x) = f (p, x)) ∧
    (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => F (1, ↑q.1, q.2)) ∧
      (∀ (S : Set X), Supported f.toFun S → Supported (fun q => F (q.1.1, q.1.2, q.2)) S) ∧
        ∀ (Q : Set ↑P),
          IsBoundarySubpolyhedron Q →
            ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => F (q.1.1, ↑q.1.2, q.2)) S'
  obtain ⟨u, hu0, hadapt, huface⟩ := reparam_exists _hP U _hUopen ρ _hρ fk:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)_hP:IsPolyhedron Pinst✝:CompactSpace XU:ι → Set X_hUopen:∀ (α : ι), IsOpen[inst✝²] (U α)ρ:PartitionOfUnity ι X_hρ:ρ.IsSubordinate Uf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∃ F,
  (∀ (p : ↑P) (x : X), F (0, p, x) = f (p, x)) ∧
    (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => F (1, ↑q.1, q.2)) ∧
      (∀ (S : Set X), Supported f.toFun S → Supported (fun q => F (q.1.1, q.1.2, q.2)) S) ∧
        ∀ (Q : Set ↑P),
          IsBoundarySubpolyhedron Q →
            ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => F (q.1.1, ↑q.1.2, q.2)) S'
  exact continuous_of_reparam U f u hu0 hadapt hufaceAll goals completed! 🐙

Theorem B (the bi-Lipschitz case):

/-- **Lemma B.0.1**, bi-Lipschitz variant (part 4 of the paper). -/
theorem biLipschitz
    {X T : Type*} [MetricSpace X] [MetricSpace T] [CompactSpace X]
    {P : Set (Fin k → ℝ)} (_hP : IsPolyhedron P)
    {ι : Type*}
    (U : ι → Set X) (_hUopen : ∀ α, IsOpen (U α))
    (ρ : PartitionOfUnity ι X univ) (_hρ : ρ.IsSubordinate U)
    (f : C(P × X, T))
    (slice : P → (X ≃ₜ T))
    (_h_slice_eq : ∀ p : P, ∀ x : X, f (p, x) = slice p x)
    (L : NNReal)
    (_hf_joint     : LipschitzWith L f.toFun)
    (_hf_slice_inv : ∀ p : P, LipschitzWith L (slice p).symm) :
    ∃ F : C(I × P × X, T), ∃ L' : NNReal, ∃ Slice : I × P → (X ≃ₜ T),
      (∀ p : P, ∀ x : X, F (0, p, x) = f (p, x)) ∧
      (∀ t : I, ∀ p : P, ∀ x : X, F (t, p, x) = Slice (t, p) x) ∧
      (∃ K : Subdivision P,
         ∀ D ∈ K.complex.facets,
            AdaptedTo U k
              (fun q : closedCell P D × X => F (1, q.1.1, q.2))) ∧
      (∀ S : Set X, Supported (f := f.toFun) S →
          Supported (fun q : (I × P) × X => F (q.1.1, q.1.2, q.2)) S) ∧
      (∀ Q : Set P, IsBoundarySubpolyhedron Q →
        ∀ S' : Set X,
          Supported (fun q : Q × X => f (q.1.1, q.2)) S' →
            Supported (fun q : (I × Q) × X => F (q.1.1, q.1.2.1, q.2)) S') ∧
      (∀ tp : I × P, LipschitzWith L' (Slice tp)) ∧
      (∀ tp : I × P, LipschitzWith L' (Slice tp).symm) := byk:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)_hP:IsPolyhedron Pι:Type u_6U:ι → Set X_hUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι X_hρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ T_h_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNReal_hf_joint:LipschitzWith L f.toFun_hf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symm⊢ ∃ F L' Slice,
  (∀ (p : ↑P) (x : X), F (0, p, x) = f (p, x)) ∧
    (∀ (t : ↑I) (p : ↑P) (x : X), F (t, p, x) = (Slice (t, p)) x) ∧
      (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => F (1, ↑q.1, q.2)) ∧
        (∀ (S : Set X), Supported f.toFun S → Supported (fun q => F (q.1.1, q.1.2, q.2)) S) ∧
          (∀ (Q : Set ↑P),
              IsBoundarySubpolyhedron Q →
                ∀ (S' : Set X),
                  Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => F (q.1.1, ↑q.1.2, q.2)) S') ∧
            (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm
  obtain ⟨u, L', Slice, hu0, hsliceEq, hadapt, huface, hLip, hLipinv⟩ :=
    reparam_biLip_exists _hP U _hUopen ρ _hρ f slice _h_slice_eq L _hf_joint _hf_slice_invk:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)_hP:IsPolyhedron Pι:Type u_6U:ι → Set X_hUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι X_hρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ T_h_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNReal_hf_joint:LipschitzWith L f.toFun_hf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmu:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm⊢ ∃ F L' Slice,
  (∀ (p : ↑P) (x : X), F (0, p, x) = f (p, x)) ∧
    (∀ (t : ↑I) (p : ↑P) (x : X), F (t, p, x) = (Slice (t, p)) x) ∧
      (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => F (1, ↑q.1, q.2)) ∧
        (∀ (S : Set X), Supported f.toFun S → Supported (fun q => F (q.1.1, q.1.2, q.2)) S) ∧
          (∀ (Q : Set ↑P),
              IsBoundarySubpolyhedron Q →
                ∀ (S' : Set X),
                  Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => F (q.1.1, ↑q.1.2, q.2)) S') ∧
            (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm
  exact biLipschitz_of_reparam U f u L' Slice hu0 hsliceEq hadapt huface hLip hLipinvAll goals completed! 🐙

end FamiliesOfMapsB01

end Submission

10. Remarks on the statement🔗

The original lemma's finiteness convention ("since X is compact, we will further assume r_\alpha = 0 for all but finitely many \alpha") appears here as a lemma (Proposition 3.1), not an assumption.
The original clause 2 ("we can decompose P = \cup_i D_i so that the restrictions to D_i \times X are adapted") is realized with the D_i the closed top cells of a genuine polyhedral subdivision of P — the stronger form needed for the chain-level applications, where adjacent cells share faces with cancelling orientations.
Of the original clause 4, the bi-Lipschitz instance is proved (Theorem B); the smooth (immersion/diffeomorphism) and PL instances are not treated. "Lipschitz family of bi-Lipschitz homeomorphisms" is made precise as: jointly Lipschitz f, slices given as homeomorphisms, inverses uniformly Lipschitz.
The role of the original general-position argument (the explicit handle formula and the count "a k-parameter family generically meets at most k walls") is played by the quantile labelling of Step 5, whose threshold-separation-versus-oscillation count (Step 5.4, (L3)) is the precise general-position mechanism; the original boundary-fixing requirements correspond to the face-respecting property (L2) together with Lemma 4.1.