The subcomplex of 𝒰-small singular chains

For an open cover 𝒰 of a space X, this file defines, in each degree n, the R-submodule

C_n^𝒰(X; R) ⊆ C_n(X; R)

of the singular chain group generated by the basis chains chainGenerator R X n σ of the 𝒰-small singular simplices σ (those whose image lies in one member of the cover, in the sense of SphereOddDegree.IsSmallSimplex).

We prove:

• SphereOddDegree.chainGenerator_mem_smallChainSubmodule — each small generator lies in the submodule;
• SphereOddDegree.smallChainSubmodule_induction — an induction/elimination principle for membership in the submodule;
• SphereOddDegree.singularBoundary_maps_smallChainSubmodule — the singular boundary maps small chains to small chains.

The boundary stability uses the singular boundary generator formula from the operator file (singularBoundary_chainGenerator_formula) and the face-smallness lemma IsSmallSimplex.face from the small-simplex file. Together these results are exactly what is needed to assemble the small singular chains into a subcomplex of the singular chain complex.

1. The small-chain submodule

noncomputable def SphereOddDegree.smallChainSubmodule (R : Type) [CommRing R] (X : TopCat) (𝒰 : OpenCoverData X) (n : ℕ) : Submodule R ↑(AffineBarycentricSubdivision.singularChainGroup R X n)

The R-submodule C_n^𝒰(X; R) ⊆ C_n(X; R) of singular chains generated by the basis chains chainGenerator R X n σ for 𝒰-small singular simplices σ.

Equations

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

theorem SphereOddDegree.chainGenerator_mem_smallChainSubmodule {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} {n : ℕ} {σ : singularSimplices X n} (hσ : IsSmallSimplex 𝒰 σ) : AffineBarycentricSubdivision.chainGenerator R X n σ ∈ smallChainSubmodule R X 𝒰 n

Each small generator lies in the small-chain submodule.

theorem SphereOddDegree.smallChainSubmodule_induction {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} {n : ℕ} {p : ↑(AffineBarycentricSubdivision.singularChainGroup R X n) → Prop} (mem : ∀ (σ : singularSimplices X n), IsSmallSimplex 𝒰 σ → p (AffineBarycentricSubdivision.chainGenerator R X n σ)) (zero : p 0) (add : ∀ (x y : ↑(AffineBarycentricSubdivision.singularChainGroup R X n)), p x → p y → p (x + y)) (smul : ∀ (a : R) (x : ↑(AffineBarycentricSubdivision.singularChainGroup R X n)), p x → p (a • x)) {c : ↑(AffineBarycentricSubdivision.singularChainGroup R X n)} (hc : c ∈ smallChainSubmodule R X 𝒰 n) : p c

Induction principle for the small-chain submodule. To prove a property p of every chain in smallChainSubmodule R X 𝒰 n, it suffices to prove it for the small generators and check that it is preserved under 0, addition and scalar multiplication.

2. Boundary stability

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

Boundary stability. The singular boundary maps the submodule of small (n+1)-chains into the submodule of small n-chains.