The small-chain complex and its inclusion into singular chains

For an open cover 𝒰 of a space X, this file packages the degree-wise small-chain submodules smallChainSubmodule R X 𝒰 n (from SmallChains.lean) into a chain complex

C_*^𝒰(X; R)

whose differential is the restriction of the singular boundary (singularBoundary_maps_smallChainSubmodule guarantees the restriction is well-defined), and defines the inclusion chain map

C_*^𝒰(X; R) ⟶ C_*(X; R).

Main definitions

• SphereOddDegree.smallBoundary — the restriction of the singular boundary to the small-chain submodules.
• SphereOddDegree.smallChainComplex — the chain complex of small singular chains.
• SphereOddDegree.smallGenerator — the small generator associated to a small singular simplex, as an element of the degree-n small-chain submodule.
• SphereOddDegree.smallChainsInclusion — the inclusion chain map into the full singular chain complex.

Main results

• SphereOddDegree.smallChainsInclusion_f_apply — the inclusion is degreewise the natural inclusion of the submodule.
• SphereOddDegree.smallChainsInclusion_generator — the inclusion sends a small generator to the corresponding singular basis chain.
• SphereOddDegree.smallChainsInclusion_boundary_compatible — the inclusion commutes with the restricted differential and the full singular boundary.

We do not prove here that smallChainsInclusion is a quasi-isomorphism.

1. The restricted boundary

noncomputable def SphereOddDegree.smallBoundary (R : Type) [CommRing R] (X : TopCat) (𝒰 : OpenCoverData X) (n : ℕ) : ↧↥(smallChainSubmodule R X 𝒰 (n + 1)) ⟶ ↧↥(smallChainSubmodule R X 𝒰 n)

The restriction of the singular boundary ∂ : C_{n+1}(X; R) → C_n(X; R) to the small-chain submodules. Well-defined by singularBoundary_maps_smallChainSubmodule.

Equations

• SphereOddDegree.smallBoundary R X 𝒰 n = ModuleCat.ofHom ((ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X n)).restrict ⋯)

@[simp]

theorem SphereOddDegree.smallBoundary_hom_apply {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} (n : ℕ) (c : ↥(smallChainSubmodule R X 𝒰 (n + 1))) : ↑((ModuleCat.Hom.hom (smallBoundary R X 𝒰 n)) c) = (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary R X n)) ↑c

theorem SphereOddDegree.smallBoundary_comp_smallBoundary {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} (n : ℕ) : CategoryTheory.CategoryStruct.comp (smallBoundary R X 𝒰 (n + 1)) (smallBoundary R X 𝒰 n) = 0

The composite ∂ ∘ ∂ of restricted boundaries vanishes.

2. The small-chain complex

noncomputable def SphereOddDegree.smallChainComplex (R : Type) [CommRing R] (X : TopCat) (𝒰 : OpenCoverData X) : ChainComplex (ModuleCat R) ℕ

The small-chain complex C_*^𝒰(X; R). In degree n the object is the small-chain submodule smallChainSubmodule R X 𝒰 n; the differential is the restricted singular boundary smallBoundary.

Equations

• SphereOddDegree.smallChainComplex R X 𝒰 = ChainComplex.of (fun (n : ℕ) => ↧↥(SphereOddDegree.smallChainSubmodule R X 𝒰 n)) (fun (n : ℕ) => SphereOddDegree.smallBoundary R X 𝒰 n) ⋯

@[simp]

theorem SphereOddDegree.smallChainComplex_X {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} (n : ℕ) : (smallChainComplex R X 𝒰).X n = ↧↥(smallChainSubmodule R X 𝒰 n)

@[simp]

theorem SphereOddDegree.smallChainComplex_d {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} (n : ℕ) : (smallChainComplex R X 𝒰).d (n + 1) n = smallBoundary R X 𝒰 n

3. Small generators

noncomputable def SphereOddDegree.smallGenerator {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} {n : ℕ} (σ : singularSimplices X n) (hσ : IsSmallSimplex 𝒰 σ) : ↥(smallChainSubmodule R X 𝒰 n)

The small generator associated to a 𝒰-small singular simplex σ, as an element of the degree-n small-chain submodule.

Equations

• SphereOddDegree.smallGenerator σ hσ = ⟨SphereOddDegree.AffineBarycentricSubdivision.chainGenerator R X n σ, ⋯⟩

@[simp]

theorem SphereOddDegree.smallGenerator_val {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} {n : ℕ} (σ : singularSimplices X n) (hσ : IsSmallSimplex 𝒰 σ) : ↑(smallGenerator σ hσ) = AffineBarycentricSubdivision.chainGenerator R X n σ

4. The inclusion chain map

noncomputable def SphereOddDegree.smallChainsInclusion (R : Type) [CommRing R] (X : TopCat) (𝒰 : OpenCoverData X) : smallChainComplex R X 𝒰 ⟶ AffineBarycentricSubdivision.singularChainComplex R X

The inclusion chain map C_*^𝒰(X; R) ⟶ C_*(X; R). Degreewise it is the natural inclusion of the small-chain submodule into the singular chain group.

Equations

• SphereOddDegree.smallChainsInclusion R X 𝒰 = { f := fun (n : ℕ) => ModuleCat.ofHom (SphereOddDegree.smallChainSubmodule R X 𝒰 n).subtype, comm' := ⋯ }

theorem SphereOddDegree.smallChainsInclusion_f_apply {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} (n : ℕ) (c : ↥(smallChainSubmodule R X 𝒰 n)) : (ModuleCat.Hom.hom ((smallChainsInclusion R X 𝒰).f n)) c = ↑c

The inclusion is, degreewise, the natural inclusion of the submodule: its underlying map sends c to its value c.val.

theorem SphereOddDegree.smallChainsInclusion_generator {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} {n : ℕ} (σ : singularSimplices X n) (hσ : IsSmallSimplex 𝒰 σ) : (ModuleCat.Hom.hom ((smallChainsInclusion R X 𝒰).f n)) (smallGenerator σ hσ) = AffineBarycentricSubdivision.chainGenerator R X n σ

The inclusion sends a small generator to the corresponding singular basis chain.

theorem SphereOddDegree.smallChainsInclusion_boundary_compatible {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} (n : ℕ) (c : ↥(smallChainSubmodule R X 𝒰 (n + 1))) : (ModuleCat.Hom.hom ((smallChainsInclusion R X 𝒰).f n)) ((ModuleCat.Hom.hom (smallBoundary R X 𝒰 n)) c) = (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary R X n)) ((ModuleCat.Hom.hom ((smallChainsInclusion R X 𝒰).f (n + 1))) c)

Boundary compatibility. The inclusion commutes with the restricted differential of the small complex and the full singular boundary.