Small Chains Homology Surjectivity

noncomputable def SphereOddDegree.homologyMapInDegree {R : Type} [CommRing R] {K L : ChainComplex (ModuleCat R) ℕ} (f : K ⟶ L) (n : ℕ) : ↑(HomologicalComplex.homology K n) → ↑(HomologicalComplex.homology L n)

The induced map on degree-n homology of a chain map, packaged as a function on the underlying homology modules.

Equations

• SphereOddDegree.homologyMapInDegree f n = ⇑(ModuleCat.Hom.hom (HomologicalComplex.homologyMap f n))

theorem SphereOddDegree.homologyMapInDegree_apply {R : Type} [CommRing R] {K L : ChainComplex (ModuleCat R) ℕ} (f : K ⟶ L) (n : ℕ) (x : ↑(HomologicalComplex.homology K n)) : homologyMapInDegree f n x = (ModuleCat.Hom.hom (HomologicalComplex.homologyMap f n)) x

theorem SphereOddDegree.homologyπ_surjective {R : Type} [CommRing R] (K : ChainComplex (ModuleCat R) ℕ) (n : ℕ) : Function.Surjective ⇑(ModuleCat.Hom.hom (HomologicalComplex.homologyπ K n))

Every degree-n homology class of a ModuleCat-valued chain complex is the image of a cycle under the homology projection homologyπ.

theorem SphereOddDegree.smallChainsInclusion_surjective_on_homology (R : Type) [CommRing R] (X : TopCat) (𝒰 : OpenCoverData X) (n : ℕ) : Function.Surjective (homologyMapInDegree (smallChainsInclusion R X 𝒰) n)

The inclusion of small chains is surjective on homology in every degree.