Chain-homotopy wrappers for singular homology

Composition, symmetry, and homotopy-equivalence wrappers around singularHomologyMap_eq_of_singularChainHomotopy. These lemmas are independent of the particular construction of the singular prism operator.

noncomputable def SphereOddDegree.singularChainHomotopyPrecomp {X Y Z : TopCat} (h : X ⟶ Y) {f g : Y ⟶ Z} (H : Homotopy (singularChainℤ.map f) (singularChainℤ.map g)) : Homotopy (singularChainℤ.map (CategoryTheory.CategoryStruct.comp h f)) (singularChainℤ.map (CategoryTheory.CategoryStruct.comp h g))

Chain-homotopy wrapper (precomposition). Transport a chain homotopy between the singular chain maps of f, g : Y ⟶ Z along precomposition with a continuous map h : X ⟶ Y, yielding a chain homotopy between the singular chain maps of h ≫ f and h ≫ g.

This is Homotopy.compLeft repackaged through the functoriality singularChainℤ.map_comp.

Equations

• SphereOddDegree.singularChainHomotopyPrecomp h H = ⋯.mpr (⋯.mpr (H.compLeft (SphereOddDegree.singularChainℤ.map h)))

noncomputable def SphereOddDegree.singularChainHomotopyPostcomp {X Y Z : TopCat} (h : Y ⟶ Z) {f g : X ⟶ Y} (H : Homotopy (singularChainℤ.map f) (singularChainℤ.map g)) : Homotopy (singularChainℤ.map (CategoryTheory.CategoryStruct.comp f h)) (singularChainℤ.map (CategoryTheory.CategoryStruct.comp g h))

Chain-homotopy wrapper (postcomposition). Transport a chain homotopy between the singular chain maps of f, g : X ⟶ Y along postcomposition with a continuous map h : Y ⟶ Z, yielding a chain homotopy between the singular chain maps of f ≫ h and g ≫ h.

This is Homotopy.compRight repackaged through singularChainℤ.map_comp.

Equations

• SphereOddDegree.singularChainHomotopyPostcomp h H = ⋯.mpr (⋯.mpr (H.compRight (SphereOddDegree.singularChainℤ.map h)))

theorem SphereOddDegree.singularHomologyℤ_map_eq_precomp {X Y Z : TopCat} (h : X ⟶ Y) {f g : Y ⟶ Z} (H : Homotopy (singularChainℤ.map f) (singularChainℤ.map g)) (n : ℕ) : (singularHomologyℤ n).map (CategoryTheory.CategoryStruct.comp h f) = (singularHomologyℤ n).map (CategoryTheory.CategoryStruct.comp h g)

Homology naturality (precomposition). If the singular chain maps of f, g : Y ⟶ Z are chain-homotopic, then for any h : X ⟶ Y the induced maps of h ≫ f and h ≫ g on the n-th integral singular homology are equal.

theorem SphereOddDegree.singularHomologyℤ_map_eq_postcomp {X Y Z : TopCat} (h : Y ⟶ Z) {f g : X ⟶ Y} (H : Homotopy (singularChainℤ.map f) (singularChainℤ.map g)) (n : ℕ) : (singularHomologyℤ n).map (CategoryTheory.CategoryStruct.comp f h) = (singularHomologyℤ n).map (CategoryTheory.CategoryStruct.comp g h)

Homology naturality (postcomposition). If the singular chain maps of f, g : X ⟶ Y are chain-homotopic, then for any h : Y ⟶ Z the induced maps of f ≫ h and g ≫ h on the n-th integral singular homology are equal.

theorem SphereOddDegree.singularHomologyℤ_map_eq_symm {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy (singularChainℤ.map f) (singularChainℤ.map g)) (n : ℕ) : (singularHomologyℤ n).map g = (singularHomologyℤ n).map f

Symmetry of the consumer. The equality on singular homology produced by a chain homotopy is symmetric: a chain homotopy between the singular chain maps of f and g gives the same homology equality read in either direction (via Homotopy.symm).

noncomputable def SphereOddDegree.singularHomologyℤIsoOfHomotopyEquiv {X Y : TopCat} (e : HomotopyEquiv (singularChainℤ.obj X) (singularChainℤ.obj Y)) (n : ℕ) : (singularHomologyℤ n).obj X ≅ (singularHomologyℤ n).obj Y

Homotopy-equivalence wrapper. A chain homotopy equivalence between the integral singular chain complexes of X and Y induces an isomorphism on the n-th integral singular homology.

This is HomotopyEquiv.toHomologyIso repackaged for the singular homology functor (the functor's object value is definitionally the homology of the chain complex). Like the rest of this file it takes the chain-level equivalence as a hypothesis: it is the homology-isomorphism consumer that homotopy invariance will feed once the prism operator upgrades a topological homotopy equivalence to a chain homotopy equivalence.

Equations

• SphereOddDegree.singularHomologyℤIsoOfHomotopyEquiv e n = e.toHomologyIso n