theorem AlgebraicTopologyI.lebesgue_covering_lemma {M : Type u_1} [PseudoMetricSpace M] [CompactSpace M] {ι : Sort u_2} {U : ι → Set M} (hU_open : ∀ (i : ι), IsOpen (U i)) (hU_cover : Set.univ ⊆ ⋃ (i : ι), U i) : ∃ ε > 0, ∀ (x : M), ∃ (i : ι), Metric.ball x ε ⊆ U i

Lemma 13.3 (Lebesgue covering lemma). Let M be a compact metric space and let U : ι → Set M be an open cover. Then there is ε > 0 such that for every x ∈ M, the ball B_ε(x) is contained in some U i.

noncomputable def SubdivisionDiameter.barycenter {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (v : Fin (n + 1) → E) : E

The barycenter of n + 1 points v 0, …, v n in a real normed space: the average (n + 1)⁻¹ · Σ v i.

theorem SubdivisionDiameter.barycenter_sub_vertex {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (v : Fin (n + 1) → E) (i : Fin (n + 1)) : barycenter n v - v i = (↑(n + 1))⁻¹ • ∑ j : Fin (n + 1), (v j - v i)

The displacement from a vertex v i to the barycenter expressed as the scaled sum of all vertex displacements v j - v i.

theorem SubdivisionDiameter.barycenter_mem_convexHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (v : Fin (n + 1) → E) : barycenter n v ∈ (convexHull ℝ) (Set.range v)

The barycenter of vertices v 0, …, v n lies in the convex hull of range v.

theorem SubdivisionDiameter.dist_barycenter_vertex_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (v : Fin (n + 1) → E) (i : Fin (n + 1)) : dist (barycenter n v) (v i) ≤ ↑n / (↑n + 1) * Metric.diam (Set.range v)

The distance from the barycenter of vertices v 0, …, v n to any vertex v i is bounded by n / (n + 1) times the diameter of the vertex set. This is the key estimate used in the proof of Lemma 13.1.

theorem SubdivisionDiameter.dist_barycenter_convexHull_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (v : Fin (n + 1) → E) (p : E) (hp : p ∈ (convexHull ℝ) (Set.range v)) : dist (barycenter n v) p ≤ ↑n / (↑n + 1) * Metric.diam (Set.range v)

The distance from the barycenter of vertices v 0, …, v n to any point of the convex hull conv(range v) is bounded by n / (n + 1) times the diameter of the vertex set.

inductive SubdivisionDiameter.IsSubdivSimplex {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} : (Fin (n + 1) → E) → Set E → Prop

Inductive predicate IsSubdivSimplex v τ characterising the vertex sets τ ⊆ E of simplices arising in the barycentric subdivision of the affine simplex with vertices v. The base case is a single point; the cone step adjoins the barycenter of v to a face subdivision.

• point {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (v : Fin 1 → E) : IsSubdivSimplex v {v 0}
• cone {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (v : Fin (n + 2) → E) (k : Fin (n + 2)) (τ : Set E) (hτ : IsSubdivSimplex (v ∘ k.succAbove) τ) : IsSubdivSimplex v (insert (barycenter (n + 1) v) τ)

theorem SubdivisionDiameter.range_comp_succAbove_subset {E : Type u_1} {n : ℕ} (v : Fin (n + 2) → E) (k : Fin (n + 2)) : Set.range (v ∘ k.succAbove) ⊆ Set.range v

Removing the k-th vertex via Fin.succAbove k produces a face whose vertex set is a subset of the original.

theorem SubdivisionDiameter.subdivSimplex_subset_convexHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {v : Fin (n + 1) → E} {τ : Set E} : IsSubdivSimplex v τ → τ ⊆ (convexHull ℝ) (Set.range v)

Every subdivision simplex of an affine simplex σ with vertices v is contained in the convex hull of range v, i.e. in σ itself.

theorem SubdivisionDiameter.subdivSimplex_isBounded {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {v : Fin (n + 1) → E} {τ : Set E} : IsSubdivSimplex v τ → Bornology.IsBounded τ

Every subdivision simplex is a bounded subset of E.

theorem SubdivisionDiameter.diam_face_le {E : Type u_1} [SeminormedAddCommGroup E] {n : ℕ} (v : Fin (n + 2) → E) (k : Fin (n + 2)) : Metric.diam (Set.range (v ∘ k.succAbove)) ≤ Metric.diam (Set.range v)

The diameter of any face of the affine simplex with vertices v is at most the diameter of range v.

theorem SubdivisionDiameter.diam_subdivSimplex_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {v : Fin (n + 1) → E} {τ : Set E} : IsSubdivSimplex v τ → Metric.diam τ ≤ ↑n / (↑n + 1) * Metric.diam (Set.range v)

Lemma 13.1 (subdivision diameter bound). For any subdivision simplex τ of the affine n-simplex σ with vertices v, diam(τ) ≤ n / (n + 1) · diam(σ).

def LocalityPrinciple.endoPow {C : ChainComplex AddCommGrpCat ℕ} (f : C ⟶ C) : ℕ → (C ⟶ C)

The k-fold composition of a chain-complex endomorphism f : C ⟶ C, i.e. f^k. Used to express iterates of the subdivision operator $^k : S_*(X) → S_*(X) from Lemma 13.4.

@[simp]

theorem LocalityPrinciple.endoPow_zero {C : ChainComplex AddCommGrpCat ℕ} (f : C ⟶ C) : endoPow f 0 = CategoryTheory.CategoryStruct.id C

The 0-th iterate of f is the identity.

@[simp]

theorem LocalityPrinciple.endoPow_succ {C : ChainComplex AddCommGrpCat ℕ} (f : C ⟶ C) (n : ℕ) : endoPow f (n + 1) = CategoryTheory.CategoryStruct.comp f (endoPow f n)

The (n + 1)-th iterate of f factors as f followed by f^n.

noncomputable def LocalityPrinciple.iteratedSubdivisionHomotopy (X : TopCat) (k : ℕ) : Homotopy (endoPow (BarycentricSubdivision.subdivisionOperator.app X) k) (CategoryTheory.CategoryStruct.id (BarycentricSubdivision.singularChainFunctorZ.obj X))

Lemma 13.4 (chain-level witness). For every k, the k-fold iterate $^k of the subdivision operator is chain-homotopic to the identity on S_*(X). The witness is built by induction on k, composing the one-step subdivision chain homotopy with the previous iterate.

theorem LocalityPrinciple.iterated_subdivision_homotopic_id (X : TopCat) (k : ℕ) : Nonempty (Homotopy (endoPow (BarycentricSubdivision.subdivisionOperator.app X) k) (CategoryTheory.CategoryStruct.id (BarycentricSubdivision.singularChainFunctorZ.obj X)))

Lemma 13.4. For every k ≥ 0, $^k ≃ 1 : S_*(X) → S_*(X) as chain maps, i.e. there exists a chain homotopy between the k-th iterate of the subdivision operator and the identity.