Each singular simplex eventually becomes small after iterated subdivision

For a singular simplex σ : Δⁿ → X and an open cover 𝒰 of X, some iterated barycentric subdivision sdᴺ([σ]) of the generator chain is a linear combination of 𝒰-small singular simplices.

The argument combines:

• the Lebesgue number of σ against 𝒰 (singularSimplex_hasLebesgueNumber_for_openCover, the project);
• the diameter shrinking of iterated barycentric subdivision (exists_iteratedSubdivision_affine_diameter_lt, the project);
• the generator expansion of the subdivision chain map.

Strategy

Every singular simplex appearing in sdᴺ([σ]) has the form σ ∘ a where a : Δⁿ → Δⁿ is an N-fold affine subdivision composite (affineCompMap). Working through the genuine linear map underlying the affine subdivision (affineSubdivLinear), we identify the vertices of this composite with the project's iterVertices, so its range has diameter < ε for N large. The Lebesgue number then forces σ ∘ a to be 𝒰-small, and the whole chain to lie in the small-chain submodule.

Main results

• support_iteratedSubdivision_generator_subset_affineSummands — sdᴺ([σ]) is a span of generators [σ ∘ a] over affine subdivision composites a.
• exists_iteratedSubdivision_generator_support_small — for some N every affine-summand simplex appearing in sdᴺ([σ]) is 𝒰-small.
• exists_iteratedSubdivision_generator_mem_smallChains — for some N, sdᴺ([σ]) lies in smallChainSubmodule.

1. The affine subdivision map as a genuine linear map

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineSubdivLinear (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (Fin (n + 1) → ℝ) →ₗ[ℝ] Fin (n + 1) → ℝ

The affine subdivision map associated to a permutation π, packaged as a genuine ℝ-linear self-map of Fin (n+1) → ℝ. On the standard simplex it restricts to affineSubdivMap n π.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivLinear_apply (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (x : Fin (n + 1) → ℝ) (j : Fin (n + 1)) : (affineSubdivLinear n π) x j = ∑ k : Fin (n + 1), x k * ↑(prefixBarycenter n π k) j

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivLinear_coe (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) : (affineSubdivLinear n π) ↑x = ↑(affineSubdivMap n π x)

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_val_eq_stepVertices (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : ↑(prefixBarycenter n π k) = BarycentricSubdivisionDiameter.stepVertices n (BarycentricSubdivisionDiameter.stdVerts n) π k

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivLinear_stdVerts (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : (affineSubdivLinear n π) (BarycentricSubdivisionDiameter.stdVerts n k) = BarycentricSubdivisionDiameter.stepVertices n (BarycentricSubdivisionDiameter.stdVerts n) π k

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineCompLinear (n N : ℕ) : (Fin N → Equiv.Perm (Fin (n + 1))) → (Fin (n + 1) → ℝ) →ₗ[ℝ] Fin (n + 1) → ℝ

Compose the barycentric subdivision linear maps selected by a permutation word.

Equations

• One or more equations did not get rendered due to their size.
• SphereOddDegree.AffineBarycentricSubdivision.affineCompLinear n 0 x_2 = LinearMap.id

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompLinear_zero (n : ℕ) (ρs : Fin 0 → Equiv.Perm (Fin (n + 1))) : affineCompLinear n 0 ρs = LinearMap.id

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompLinear_succ (n N : ℕ) (ρs : Fin (N + 1) → Equiv.Perm (Fin (n + 1))) : affineCompLinear n (N + 1) ρs = (affineCompLinear n N fun (i : Fin N) => ρs i.castSucc) ∘ₗ affineSubdivLinear n (ρs (Fin.last N))

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompLinear_stdVerts (n N : ℕ) (ρs : Fin N → Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : (affineCompLinear n N ρs) (BarycentricSubdivisionDiameter.stdVerts n k) = BarycentricSubdivisionDiameter.iterVertices n N ρs (BarycentricSubdivisionDiameter.stdVerts n) k

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (n N : ℕ) : (Fin N → Equiv.Perm (Fin (n + 1))) → C(↑(Delta n), ↑(Delta n))

The continuous simplex self-map associated with an iterated subdivision word.

Equations

• One or more equations did not get rendered due to their size.
• SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n 0 x_2 = ContinuousMap.id ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompMap_zero (n : ℕ) (ρs : Fin 0 → Equiv.Perm (Fin (n + 1))) : affineCompMap n 0 ρs = ContinuousMap.id ↑(Delta n)

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompMap_succ (n N : ℕ) (ρs : Fin (N + 1) → Equiv.Perm (Fin (n + 1))) : affineCompMap n (N + 1) ρs = (affineCompMap n N fun (i : Fin N) => ρs i.castSucc).comp (affineSubdivContinuousMap n (ρs (Fin.last N)))

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompMap_coe (n N : ℕ) (ρs : Fin N → Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) : ↑((affineCompMap n N ρs) x) = (affineCompLinear n N ρs) ↑x

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompMap_snoc (n N : ℕ) (ρs : Fin N → Equiv.Perm (Fin (n + 1))) (π : Equiv.Perm (Fin (n + 1))) : affineCompMap n (N + 1) (Fin.snoc ρs π) = (affineCompMap n N ρs).comp (affineSubdivContinuousMap n π)

theorem SphereOddDegree.AffineBarycentricSubdivision.range_affineCompMap_val (n N : ℕ) (ρs : Fin N → Equiv.Perm (Fin (n + 1))) : Subtype.val '' Set.range ⇑(affineCompMap n N ρs) = (convexHull ℝ) (Set.range (BarycentricSubdivisionDiameter.iterVertices n N ρs (BarycentricSubdivisionDiameter.stdVerts n)))

theorem SphereOddDegree.AffineBarycentricSubdivision.diam_range_affineCompMap (n N : ℕ) (ρs : Fin N → Equiv.Perm (Fin (n + 1))) : Metric.diam (Set.range ⇑(affineCompMap n N ρs)) = Metric.diam (Set.range (BarycentricSubdivisionDiameter.iterVertices n N ρs (BarycentricSubdivisionDiameter.stdVerts n)))

theorem SphereOddDegree.AffineBarycentricSubdivision.exists_diam_range_affineCompMap_lt (n : ℕ) (eps : ℝ) (heps : 0 < eps) : ∃ (N : ℕ), ∀ (ρs : Fin N → Equiv.Perm (Fin (n + 1))), Metric.diam (Set.range ⇑(affineCompMap n N ρs)) < eps

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineSummandSimplex {X : TopCat} (n N : ℕ) (σ : singularSimplices X n) (ρs : Fin N → Equiv.Perm (Fin (n + 1))) : singularSimplices X n

A singular simplex precomposed with one iterated barycentric subdivision map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.mvSimplexMap_affineSummandSimplex {X : TopCat} (n N : ℕ) (σ : singularSimplices X n) (ρs : Fin N → Equiv.Perm (Fin (n + 1))) : mvSimplexMap (affineSummandSimplex n N σ ρs) = (mvSimplexMap σ).comp (affineCompMap n N ρs)

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSummandSimplex_zero {X : TopCat} (n : ℕ) (σ : singularSimplices X n) (ρs : Fin 0 → Equiv.Perm (Fin (n + 1))) : affineSummandSimplex n 0 σ ρs = σ

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivSimplex_affineSummandSimplex {X : TopCat} (n N : ℕ) (σ : singularSimplices X n) (ρs : Fin N → Equiv.Perm (Fin (n + 1))) (π : Equiv.Perm (Fin (n + 1))) : barycentricSubdivSimplex X n π (affineSummandSimplex n N σ ρs) = affineSummandSimplex n (N + 1) σ (Fin.snoc ρs π)

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap_succ' (R : Type) [CommRing R] (X : TopCat) (N n : ℕ) (c : ↑(singularChainGroup R X n)) : (barycentricSubdivisionIterLinearMap R X (N + 1) n) c = (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) ((barycentricSubdivisionIterLinearMap R X N n) c)

theorem SphereOddDegree.AffineBarycentricSubdivision.support_iteratedSubdivision_generator_subset_affineSummands {X : TopCat} (R : Type) [CommRing R] (n N : ℕ) (σ : singularSimplices X n) : (barycentricSubdivisionIterLinearMap R X N n) (chainGenerator R X n σ) ∈ Submodule.span R {c : ↑(singularChainGroup R X n) | ∃ (ρs : Fin N → Equiv.Perm (Fin (n + 1))), chainGenerator R X n (affineSummandSimplex n N σ ρs) = c}

theorem SphereOddDegree.AffineBarycentricSubdivision.exists_iteratedSubdivision_generator_support_small {X : TopCat} (n : ℕ) (σ : singularSimplices X n) (𝒰 : OpenCoverData X) : ∃ (N : ℕ), ∀ (ρs : Fin N → Equiv.Perm (Fin (n + 1))), IsSmallSimplex 𝒰 (affineSummandSimplex n N σ ρs)

theorem SphereOddDegree.AffineBarycentricSubdivision.exists_iteratedSubdivision_generator_mem_smallChains {X : TopCat} (R : Type) [CommRing R] (n : ℕ) (σ : singularSimplices X n) (𝒰 : OpenCoverData X) : ∃ (N : ℕ), (barycentricSubdivisionIterLinearMap R X N n) (chainGenerator R X n σ) ∈ smallChainSubmodule R X 𝒰 n