Adapting families of maps to open covers

DefinitionFamilies of maps supported on a set#✓fully proved

Let \(X\) and \(T\) be topological spaces and \(P\) a set. A family of maps \(f : P \times X \to T\) is supported on a set \(S \subseteq X\) when it does not depend on the parameter outside \(S\): \(f(p, x) = f(p', x)\) for all \(p, p' \in P\) and all \(x \notin S\).

def Supported {P : Type*} (f : P × X → T) (S : Set X) : Prop :=
  ∀ p p' : P, ∀ x ∉ S, f (p, x) = f (p', x)

Used by 3

Used byAdapted families of maps · Morrison–Walker lemma on adapting families of maps, bi-Lipschitz case · Morrison–Walker lemma on adapting families of maps to an open cover

DefinitionAdapted families of maps#✓fully proved

Let \(X\) and \(T\) be topological spaces, \(P\) a set, \(U = (U_\alpha)_{\alpha \in \iota}\) a family of subsets of \(X\) and \(k\) a natural number. A family of maps \(f : P \times X \to T\) is adapted to \(U\) with bound \(k\) when there is a finite set \(A\) of at most \(k\) indices such that \(f\) is supported on \(\bigcup_{\alpha \in A} U_\alpha\).

def AdaptedTo {P : Type*} (U : ι → Set X) (k : ℕ) (f : P × X → T) : Prop :=
  ∃ A : Finset ι, A.card ≤ k ∧ Supported f (⋃ α ∈ A, U α)

Uses 1 · Used by 2

Statement usesFamilies of maps supported on a set

Used byMorrison–Walker lemma on adapting families of maps, bi-Lipschitz case · Morrison–Walker lemma on adapting families of maps to an open cover

DefinitionConvex linear polyhedra#✓fully proved

A subset \(P \subseteq \mathbb{R}^k\) is a convex linear polyhedron when it is the convex hull of a finite set of points (equivalently, a bounded intersection of finitely many closed half-spaces).

def IsPolyhedron (P : Set (Fin k → ℝ)) : Prop :=
  ∃ S : Finset (Fin k → ℝ), P = convexHull ℝ (S : Set _)

Used by 2

Used byMorrison–Walker lemma on adapting families of maps, bi-Lipschitz case · Morrison–Walker lemma on adapting families of maps to an open cover

StructurePolyhedral subdivisions#✓fully proved

A polyhedral subdivision of a set \(P \subseteq \mathbb{R}^k\) is a geometric simplicial complex in \(\mathbb{R}^k\) with finitely many faces whose underlying space equals \(P\).

structure Subdivision (P : Set (Fin k → ℝ)) where
  complex      : SimplicialComplex ℝ (Fin k → ℝ)
  faces_finite : complex.faces.Finite
  space_eq     : complex.space = P

Used by 2

Used byMorrison–Walker lemma on adapting families of maps, bi-Lipschitz case · Morrison–Walker lemma on adapting families of maps to an open cover

DefinitionClosed cells#✓fully proved

Let \(P \subseteq \mathbb{R}^k\) and let \(D \subseteq \mathbb{R}^k\) be a finite set (typically the vertex set of a face of a subdivision of \(P\)). The closed cell of \(D\) in \(P\) is the set of points of \(P\) that lie in the convex hull of \(D\), viewed as a subset of \(P\).

def closedCell (P : Set (Fin k → ℝ)) (D : Finset (Fin k → ℝ)) : Set P :=
  { p | (p : Fin k → ℝ) ∈ convexHull ℝ (D : Set (Fin k → ℝ)) }

Used by 2

Used byMorrison–Walker lemma on adapting families of maps, bi-Lipschitz case · Morrison–Walker lemma on adapting families of maps to an open cover

DefinitionBoundary subpolyhedra#✓fully proved

Let \(P \subseteq \mathbb{R}^k\). A subset \(Q \subseteq P\) is a boundary subpolyhedron of \(P\) when \(Q\) is the convex hull of a finite set of points of \(\mathbb{R}^k\), \(Q\) lies in the intrinsic frontier (relative boundary) of \(P\), and \(Q\) is a face of \(P\): whenever a point of \(Q\) lies in the open segment between two points of \(P\), both of those points lie in \(Q\).

The face condition matches the paper's "convex linear subpolyhedron of \(\partial P\)"; without it a single non-vertex point of the boundary of \(P\) would qualify.

def IsBoundarySubpolyhedron {P : Set (Fin k → ℝ)} (Q : Set P) : Prop :=
  (∃ S : Finset (Fin k → ℝ),
      ((↑) : P → Fin k → ℝ) '' Q = convexHull ℝ (S : Set (Fin k → ℝ))) ∧
    ((↑) : P → Fin k → ℝ) '' Q ⊆ intrinsicFrontier ℝ P ∧
    IsExtreme ℝ P (((↑) : P → Fin k → ℝ) '' Q)

Used by 2

Used byMorrison–Walker lemma on adapting families of maps, bi-Lipschitz case · Morrison–Walker lemma on adapting families of maps to an open cover

TheoremMorrison–Walker lemma on adapting families of maps to an open cover#●ready to prove

Let \(X\) be a compact topological space, \(T\) a topological space, \(P \subseteq \mathbb{R}^k\) a convex linear polyhedron, \((U_\alpha)_{\alpha \in \iota}\) a family of open subsets of \(X\), and \(\rho\) a partition of unity on \(X\) indexed by \(\iota\) and subordinate to \(U\) (the closed support of \(\rho_\alpha\) lies in \(U_\alpha\)). Then for every continuous map \(f : P \times X \to T\) there is a continuous map \(F : [0, 1] \times P \times X \to T\) such that: (i) \(F(0, p, x) = f(p, x)\) for all \(p \in P\) and \(x \in X\); (ii) there is a polyhedral subdivision \(K\) of \(P\) such that, for every facet (maximal face) \(D\) of \(K\), the family \((p, x) \mapsto F(1, p, x)\) with \(p\) in the closed cell of \(D\) is adapted to \(U\) with bound \(k\); (iii) for every \(S \subseteq X\), if \(f\) is supported on \(S\), then \(F\), as a family with parameter \((t, p) \in [0, 1] \times P\), is supported on \(S\); (iv) for every boundary subpolyhedron \(Q\) of \(P\) and every \(S' \subseteq X\), if the restriction of \(f\) to \(Q \times X\) is supported on \(S'\), then the restriction of \(F\) to \([0, 1] \times Q \times X\), as a family with parameter \((t, q) \in [0, 1] \times Q\), is supported on \(S'\).

MathlibExt.Topology.FamiliesOfMapsB01Wanted.FamiliesOfMapsB01.continuous · 18 lines

public theorem_wanted 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')

Sources

• S. Morrison and K. Walker, The Blob Complex, arXiv:1009.5025, Appendix B, Lemma B.0.1 (pp. 93–96): https://arxiv.org/pdf/1009.5025. Problem families_of_maps_b01 of the lean-eval benchmark.

Uses 6

Statement usesAdapted families of maps · Boundary subpolyhedra · Convex linear polyhedra · Polyhedral subdivisions · Families of maps supported on a set · Closed cells

TheoremMorrison–Walker lemma on adapting families of maps, bi-Lipschitz case#●ready to prove

Let \(X\) be a compact metric space, \(T\) a metric space, \(P \subseteq \mathbb{R}^k\) a convex linear polyhedron, \((U_\alpha)_{\alpha \in \iota}\) a family of open subsets of \(X\), and \(\rho\) a partition of unity on \(X\) indexed by \(\iota\) and subordinate to \(U\). Let \(f : P \times X \to T\) be continuous and suppose that for each \(p \in P\) the map \(x \mapsto f(p, x)\) is a homeomorphism \(h_p : X \to T\), and that for some constant \(L \ge 0\) the map \(f\) is \(L\)-Lipschitz on \(P \times X\) (for the sup metrics on \(\mathbb{R}^k\) and on \(P \times X\)) and every inverse \(h_p^{-1}\) is \(L\)-Lipschitz. Then there are a continuous map \(F : [0, 1] \times P \times X \to T\), a constant \(L' \ge 0\) and homeomorphisms \(H_{t,p} : X \to T\) for \((t, p) \in [0, 1] \times P\) such that: (i) \(F(0, p, x) = f(p, x)\) for all \(p\) and \(x\); (ii) \(F(t, p, x) = H_{t,p}(x)\) for all \(t\), \(p\), \(x\); (iii) there is a polyhedral subdivision \(K\) of \(P\) such that, for every facet (maximal face) \(D\) of \(K\), the family \((p, x) \mapsto F(1, p, x)\) with \(p\) in the closed cell of \(D\) is adapted to \(U\) with bound \(k\); (iv) for every \(S \subseteq X\), if \(f\) is supported on \(S\), then \(F\), as a family with parameter \((t, p) \in [0, 1] \times P\), is supported on \(S\); (v) for every boundary subpolyhedron \(Q\) of \(P\) and every \(S' \subseteq X\), if the restriction of \(f\) to \(Q \times X\) is supported on \(S'\), then the restriction of \(F\) to \([0, 1] \times Q \times X\), as a family with parameter \((t, q) \in [0, 1] \times Q\), is supported on \(S'\); and (vi) every \(H_{t,p}\) and every inverse \(H_{t,p}^{-1}\) is \(L'\)-Lipschitz.

MathlibExt.Topology.FamiliesOfMapsB01Wanted.FamiliesOfMapsB01.biLipschitz · 27 lines

public theorem_wanted 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)

Sources

• S. Morrison and K. Walker, The Blob Complex, arXiv:1009.5025, Appendix B, Lemma B.0.1 (pp. 93–96): https://arxiv.org/pdf/1009.5025. Problem families_of_maps_b01 of the lean-eval benchmark.

Uses 6

Statement usesAdapted families of maps · Boundary subpolyhedra · Convex linear polyhedra · Polyhedral subdivisions · Families of maps supported on a set · Closed cells

6 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.