Smallness/carrier control of the subdivision homotopy terms

This file proves the carrier control needed for the small-simplices quasi-isomorphism: the chain-homotopy witnesses relating iterated barycentric subdivision to the identity become small (with respect to a given open cover) when applied to small chains.

The accumulated homotopy operator was built in BarycentricSubdivisionIter.lean as

H^(N) = barycentricSubdivisionIterHomotopyLinearMap R X N
 = Σ_{r=0}^{N-1} (sd^r) ∘ H,

with H = barycentricSubdivisionHomotopyLinearMap the one-step homotopy and sd^r = barycentricSubdivisionIterLinearMap. Its chain-level boundary formula barycentricSubdivisionIter_boundary_formula reads c - sd^N(c) = ∂(H^(N) c) + H^(N)(∂ c).

Key geometric fact (carrier control)

The one-step homotopy H([σ]) is the pushforward, along σ, of a fixed universal chain T_n on the standard simplex Δⁿ. Therefore every simplex appearing in H([σ]) has image contained in image(σ). Consequently, if σ is 𝒰-small then H([σ]) is a 𝒰-small chain; and the same holds for the iterated homotopy, because sd also preserves smallness (carriers of a subdivision summand lie inside the carrier of the original simplex).

The clean statement underlying all of this is:

• singularChainMap_mem_smallChainSubmodule — the pushforward of any chain along a continuous map f whose image lies inside a member of the cover is a small chain.

From it we deduce:

• subdivisionHomotopy_preserves_smallChains — the one-step homotopy H maps small chains to small chains.
• iteratedSubdivisionHomotopy_preserves_smallChains — the accumulated homotopy H^(N) maps small chains to small chains (for every N).

Finally we combine with the project (exists_iteratedSubdivision_chain_mem_smallChains):

• exists_iteratedSubdivision_homotopy_mem_smallChains — for every chain c there is N such that sd^N(c) is small and the homotopy term of the small subdivided chain H^(N)(sd^N c) is small.
• exists_iteratedSubdivision_homotopy_boundary_mem_smallChains — the injectivity tool: if b has a small boundary z = ∂b (e.g. z is a small cycle bounding b globally), then there is N with both sd^N(b) small and the homotopy chain H^(N)(z) small. By the boundary formula these are exactly the chains needed to rewrite z as a boundary inside the small subcomplex.

Faithfulness note

For an arbitrary (non-small) chain c, the homotopy term H^(N)(c) is not small: the boundary formula forces ∂(H^(N) c) + H^(N)(∂ c) = c - sd^N(c), so the carriers of H^(N)(c) must cover the carriers of c itself. This is why the exists-theorems control the homotopy term of the subdivided/small chain (resp. of the small boundary z), which is exactly what the project require; we do not state the (false) claim that H^(N)(c) is small for arbitrary c.

1. Carrier control for pushforward chains

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_mem_smallChainSubmodule {X : TopCat} (R : Type) [CommRing R] {Y : TopCat} (𝒰 : OpenCoverData X) (n : ℕ) (f : Y ⟶ X) (hf : ∃ U ∈ 𝒰.sets, Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ⊆ U) (c : ↑(singularChainGroup R Y n)) : (ModuleCat.Hom.hom (singularChainMap R f n)) c ∈ smallChainSubmodule R X 𝒰 n

2. The one-step homotopy preserves small chains

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

3. The accumulated homotopy preserves small chains

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

4. Existence theorems combining shrinking and carrier control

theorem SphereOddDegree.AffineBarycentricSubdivision.exists_iteratedSubdivision_homotopy_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 ∧ (barycentricSubdivisionIterHomotopyLinearMap R X N n) ((barycentricSubdivisionIterLinearMap R X N n) c) ∈ smallChainSubmodule R X 𝒰 (n + 1)

Subdivision-and-homotopy smallness. For every chain c there is N with sd^N(c) small and the homotopy term of the (now small) subdivided chain, H^(N)(sd^N c), small.

(The homotopy term is taken of the small subdivided chain sd^N c; this is the form that is actually small. See the faithfulness note in the module docstring.)

theorem SphereOddDegree.AffineBarycentricSubdivision.exists_iteratedSubdivision_homotopy_boundary_mem_smallChains {X : TopCat} (𝒰 : OpenCoverData X) (R : Type) [CommRing R] (n : ℕ) (b : ↑(singularChainGroup R X (n + 1))) (hz : (ModuleCat.Hom.hom (singularBoundary R X n)) b ∈ smallChainSubmodule R X 𝒰 n) : ∃ (N : ℕ), (barycentricSubdivisionIterLinearMap R X N (n + 1)) b ∈ smallChainSubmodule R X 𝒰 (n + 1) ∧ (barycentricSubdivisionIterHomotopyLinearMap R X N n) ((ModuleCat.Hom.hom (singularBoundary R X n)) b) ∈ smallChainSubmodule R X 𝒰 (n + 1)

Injectivity tool: small boundary witness. Suppose b is an (n+1)-chain whose boundary z = ∂b is 𝒰-small (for instance, z is a small cycle that bounds b globally). Then there is N such that both

• sd^N(b) is a small (n+1)-chain, and
• the homotopy chain H^(N)(z) = H^(N)(∂b) relating sd^N(z) to z is a small (n+1)-chain.

Combined with the boundary formula z - sd^N(z) = ∂(H^(N) z) + H^(N)(∂ z) (and ∂z = 0 when z is a cycle), these are exactly the small chains needed to exhibit z as a boundary inside the small subcomplex in the project.