Iterated Subdivision Small Chains

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.mvSimplexMap_barycentricSubdivSimplex {X : TopCat} (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (σ : singularSimplices X n) : mvSimplexMap (barycentricSubdivSimplex X n π σ) = (mvSimplexMap σ).comp (affineSubdivContinuousMap n π)

theorem SphereOddDegree.AffineBarycentricSubdivision.IsSmallSimplex.barycentricSubdivSimplex {X : TopCat} {𝒰 : OpenCoverData X} {n : ℕ} {σ : singularSimplices X n} (hσ : IsSmallSimplex 𝒰 σ) (π : Equiv.Perm (Fin (n + 1))) : IsSmallSimplex 𝒰 (AffineBarycentricSubdivision.barycentricSubdivSimplex X n π σ)

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivision_maps_smallChainSubmodule {X : TopCat} (R : Type) [CommRing R] (𝒰 : OpenCoverData X) (n : ℕ) (c : ↑(singularChainGroup R X n)) : c ∈ smallChainSubmodule R X 𝒰 n → (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) c ∈ smallChainSubmodule R X 𝒰 n

One subdivision preserves small chains. The degree-wise barycentric subdivision maps the small-chain submodule into itself.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIter_maps_smallChainSubmodule {X : TopCat} (R : Type) [CommRing R] (𝒰 : OpenCoverData X) (N n : ℕ) (c : ↑(singularChainGroup R X n)) : c ∈ smallChainSubmodule R X 𝒰 n → (barycentricSubdivisionIterLinearMap R X N n) c ∈ smallChainSubmodule R X 𝒰 n

Every iterate preserves small chains.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap_add {X : TopCat} (R : Type) [CommRing R] (a b n : ℕ) (c : ↑(singularChainGroup R X n)) : (barycentricSubdivisionIterLinearMap R X (a + b) n) c = (barycentricSubdivisionIterLinearMap R X a n) ((barycentricSubdivisionIterLinearMap R X b n) c)

sd^(a+b) = sd^a ∘ sd^b degree-wise.

theorem SphereOddDegree.AffineBarycentricSubdivision.sdIter_mem_smallChainSubmodule_mono {X : TopCat} (R : Type) [CommRing R] (𝒰 : OpenCoverData X) {N M n : ℕ} (hNM : N ≤ M) {c : ↑(singularChainGroup R X n)} (hc : (barycentricSubdivisionIterLinearMap R X N n) c ∈ smallChainSubmodule R X 𝒰 n) : (barycentricSubdivisionIterLinearMap R X M n) c ∈ smallChainSubmodule R X 𝒰 n

Monotonicity in the number of subdivisions. If sd^N c is a small chain and N ≤ M, then sd^M c is a small chain.

theorem SphereOddDegree.AffineBarycentricSubdivision.chainGenerator_span_top {X : TopCat} (R : Type) [CommRing R] (n : ℕ) : Submodule.span R (Set.range (chainGenerator R X n)) = ⊤

The basis generators [σ] span the singular chain group (it is the free R-module on singular simplices).

theorem SphereOddDegree.AffineBarycentricSubdivision.exists_iteratedSubdivision_chain_mem_smallChains {X : TopCat} (𝒰 : OpenCoverData X) (R : Type) [CommRing R] (n : ℕ) (c : ↑(singularChainGroup R X n)) : ∃ (N : ℕ), (barycentricSubdivisionIterLinearMap R X N n) c ∈ smallChainSubmodule R X 𝒰 n

Main theorem. For every singular chain c and every open cover 𝒰, some iterated barycentric subdivision sdᴺ(c) lies in the submodule of 𝒰-small chains.