Iterated barycentric subdivision produces small simplices

Points of the standard simplex StdSimplex ℝ N on a finite type N are measured by their weight vectors ⇑w.weights : N → ℝ with the sup metric, which induces the topology of the simplex. If the vertices of an affine k-simplex are pairwise at distance at most d, then the vertices of each simplex of its barycentric subdivision are pairwise at distance at most k / (k + 1) * d: they are the barycenters of a decreasing chain of faces, and the barycenter of a face with at most k + 1 vertices lies within k / (k + 1) * d of each of its vertices. Since all points of the simplex are at distance at most 1, the vertex tuples of the n-fold iterated subdivision of any affine k-chain are pairwise at distance at most (k / (k + 1)) ^ n.

Combined with the Lebesgue number lemma, this shows that for every open cover U of a space X and every singular simplex σ : Δᵐ → X, all affine simplices of a sufficiently fine iterated subdivision are carried by σ into a single member of U. Since pushing affine chains forward along σ intertwines their subdivision with the barycentric subdivision of singular chains (TauCeti.AffineChain.singularChain_subdivision), this is the statement that every singular simplex becomes subordinate to U after sufficiently many barycentric subdivisions.

Main results

• TauCeti.BarycentricSubdivision.dist_weights_affineMapMk_vertex_le_of_le: vertices indexed by i ≤ j satisfy the finer bound (j - i) / (k + 1 - i) * d.
• TauCeti.BarycentricSubdivision.dist_weights_affineMapMk_vertex_le: subdivision shrinks the distances between the vertices of an affine simplex by the factor k / (k + 1).
• TauCeti.AffineChain.dist_weights_le_of_mem_support_subdivision_iterate: the vertex tuples of the n-fold subdivision of an affine k-chain are pairwise at distance at most (k / (k + 1)) ^ n.
• ContinuousMap.exists_pos_forall_range_subset_of_dist_weights_lt: a Lebesgue number for an open cover pulled back along a singular simplex, bounding the distances between vertices.
• ContinuousMap.exists_forall_mem_support_subdivision_iterate_range_subset: every affine simplex of a sufficiently fine iterated subdivision is carried into a member of the cover.

References

• A. Hatcher, Algebraic Topology, Section 2.1, proof of Proposition 2.21, steps (2) and (4).

theorem TauCeti.BarycentricSubdivision.dist_weights_affineMapMk_vertex_le_of_le {N : Type u_1} [Fintype N] {k : ℕ} (v : Fin (k + 1) → Convexity.StdSimplex ℝ N) {d : ℝ} (hd : ∀ (i j : Fin (k + 1)), dist ⇑(v i).weights ⇑(v j).weights ≤ d) (π : Equiv.Perm (Fin (k + 1))) {i j : Fin (k + 1)} (hij : i ≤ j) : dist ⇑((Convexity.StdSimplex.affineMapMk v) (vertex π j)).weights ⇑((Convexity.StdSimplex.affineMapMk v) (vertex π i)).weights ≤ (↑↑j - ↑↑i) / (↑k + 1 - ↑↑i) * d

The distance between subdivision vertices indexed by i ≤ j is bounded by (j - i) / (k + 1 - i) times the original diameter bound.

theorem TauCeti.BarycentricSubdivision.dist_weights_affineMapMk_vertex_le {N : Type u_1} [Fintype N] {k : ℕ} (v : Fin (k + 1) → Convexity.StdSimplex ℝ N) {d : ℝ} (hd : ∀ (i j : Fin (k + 1)), dist ⇑(v i).weights ⇑(v j).weights ≤ d) (π : Equiv.Perm (Fin (k + 1))) (i j : Fin (k + 1)) : dist ⇑((Convexity.StdSimplex.affineMapMk v) (vertex π i)).weights ⇑((Convexity.StdSimplex.affineMapMk v) (vertex π j)).weights ≤ ↑k / (↑k + 1) * d

Barycentric subdivision shrinks simplices. If the vertices of an affine k-simplex in a standard simplex are pairwise at distance at most d, then so are the vertices of each simplex of its barycentric subdivision, up to the factor k / (k + 1).

theorem TauCeti.AffineChain.dist_weights_le_of_mem_support_subdivision {N : Type u_1} [Fintype N] {k : ℕ} {c : (Fin (k + 1) → Convexity.StdSimplex ℝ N) →₀ ℤ} {d : ℝ} (hc : ∀ v ∈ c.support, ∀ (i j : Fin (k + 1)), dist ⇑(v i).weights ⇑(v j).weights ≤ d) {u : Fin (k + 1) → Convexity.StdSimplex ℝ N} (hu : u ∈ ((subdivision (Convexity.StdSimplex ℝ N) k) c).support) (i j : Fin (k + 1)) : dist ⇑(u i).weights ⇑(u j).weights ≤ ↑k / (↑k + 1) * d

If the vertex tuples in the support of an affine k-chain are pairwise at distance at most d, then those of its barycentric subdivision are pairwise at distance at most k / (k + 1) * d.

theorem TauCeti.AffineChain.dist_weights_le_of_mem_support_subdivision_iterate {N : Type u_1} [Fintype N] {k n : ℕ} {c : (Fin (k + 1) → Convexity.StdSimplex ℝ N) →₀ ℤ} {u : Fin (k + 1) → Convexity.StdSimplex ℝ N} (hu : u ∈ ((⇑(subdivision (Convexity.StdSimplex ℝ N) k))^[n] c).support) (i j : Fin (k + 1)) : dist ⇑(u i).weights ⇑(u j).weights ≤ (↑k / (↑k + 1)) ^ n

The vertex tuples of the n-fold barycentric subdivision of an affine k-chain in a standard simplex are pairwise at distance at most (k / (k + 1)) ^ n.

theorem ContinuousMap.exists_pos_forall_range_subset_of_dist_weights_lt {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] (σ : C(Convexity.StdSimplex ℝ N, X)) {ι : Type u_3} {U : ι → Set X} (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) : ∃ δ > 0, ∀ {k : ℕ} (v : Fin (k + 1) → Convexity.StdSimplex ℝ N), (∀ (i j : Fin (k + 1)), dist ⇑(v i).weights ⇑(v j).weights < δ) → ∃ (i : ι), Set.range ⇑(σ.comp (Convexity.StdSimplex.continuousAffineMapMk v)) ⊆ U i

Lebesgue number of a singular simplex. For an open cover U of X and a singular simplex σ : StdSimplex ℝ N → X, there is δ > 0 such that every affine simplex whose vertices are pairwise at distance less than δ is carried by σ into a single member of U.

theorem ContinuousMap.exists_forall_mem_support_subdivision_iterate_range_subset {N : Type u_1} [Finite N] {X : Type u_2} [TopologicalSpace X] (σ : C(Convexity.StdSimplex ℝ N, X)) {ι : Type u_3} {U : ι → Set X} (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) (k : ℕ) : ∃ (n₀ : ℕ), ∀ n ≥ n₀, ∀ (c : (Fin (k + 1) → Convexity.StdSimplex ℝ N) →₀ ℤ), ∀ u ∈ ((⇑(TauCeti.AffineChain.subdivision (Convexity.StdSimplex ℝ N) k))^[n] c).support, ∃ (i : ι), Set.range ⇑(σ.comp (Convexity.StdSimplex.continuousAffineMapMk u)) ⊆ U i

Iterated subdivision is eventually subordinate to an open cover. For an open cover U of X, a singular simplex σ : StdSimplex ℝ N → X and a dimension k, there is n₀ such that for all n ≥ n₀ and every affine k-chain c, each affine simplex of the n-fold barycentric subdivision of c is carried by σ into a single member of U.