Homotopy invariance of relative singular homology

A homotopy between maps of topological pairs induces a chain homotopy between the induced maps of relative singular chain complexes, so homotopic maps of pairs induce the same map on relative singular homology, and maps of pairs that are inverse to each other up to homotopy induce isomorphisms on it. This is the homotopy axiom of Eilenberg--Steenrod for the relative singular theory. In the absolute case, a homotopy equivalence of spaces induces an isomorphism on singular homology (ContinuousMap.HomotopyEquiv.singularHomologyIso).

The homotopy is transported to the singular simplicial sets of the two spaces, where the compatibility of the two simplicial homotopies over the inclusion of the subspace descends the chain homotopy to the relative chain complexes. The absolute case is Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean (F. Odermatt, J. Riou), whose proof plan through TopCat.Homotopy.toSSet this file follows for pairs.

The source is Eilenberg--Steenrod, Foundations of Algebraic Topology, Chapter VII, where the homotopy axiom is verified for the singular theory; see also Hatcher, Algebraic Topology, §2.1, Theorem 2.10 and its relative form.

noncomputable def TopPair.Homotopy.singularChainComplexMap {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : _root_.Homotopy (TopPair.singularChainComplexMap f R) (TopPair.singularChainComplexMap g R)

A homotopy between maps of topological pairs induces a chain homotopy between the induced maps of relative singular chain complexes.

Equations

• H.singularChainComplexMap R = H.toSSetPair.chainComplexMap R

@[simp]

theorem TopPair.Homotopy.singularChainComplexMap_hom {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (p q : ℕ) : CategoryTheory.CategoryStruct.comp ((P.singularChainComplexπ R).f p) ((H.singularChainComplexMap R).hom p q) = CategoryTheory.CategoryStruct.comp ((H.fst.toSSet.chainComplexMap R).hom p q) ((P'.singularChainComplexπ R).f q)

@[simp]

theorem TopPair.Homotopy.singularChainComplexMap_hom_assoc {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (p q : ℕ) {Z : C} (h : (P'.singularChainComplex R).X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((P.singularChainComplexπ R).f p) (CategoryTheory.CategoryStruct.comp ((H.singularChainComplexMap R).hom p q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((H.fst.toSSet.chainComplexMap R).hom p q) ((P'.singularChainComplexπ R).f q)) h

theorem TopPair.Homotopy.congr_singularHomologyMap {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : TopPair.singularHomologyMap f R n = TopPair.singularHomologyMap g R n

Homotopic maps of topological pairs induce the same map on relative singular homology.

theorem TopPair.isIso_singularHomologyMap {P P' : TopPair} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (f : P ⟶ P') (f' : P' ⟶ P) (H : Homotopy (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.id P)) (H' : Homotopy (CategoryTheory.CategoryStruct.comp f' f) (CategoryTheory.CategoryStruct.id P')) (R : C) (n : ℕ) : CategoryTheory.IsIso (TopPair.singularHomologyMap f R n)

Maps of topological pairs which are inverse to each other up to homotopy induce isomorphisms on relative singular homology.

noncomputable def ContinuousMap.HomotopyEquiv.singularHomologyIso {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (n : ℕ) : ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj ↧X ≅ ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj ↧Y

A homotopy equivalence induces an isomorphism on singular homology in every degree, with inverse induced by the homotopy inverse.

Equations

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

@[simp]

theorem ContinuousMap.HomotopyEquiv.singularHomologyIso_hom {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (n : ℕ) : (e.singularHomologyIso R n).hom = ((AlgebraicTopology.singularHomologyFunctor C n).obj R).map (TopCat.ofHom e.toFun)

@[simp]

theorem ContinuousMap.HomotopyEquiv.singularHomologyIso_inv {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (n : ℕ) : (e.singularHomologyIso R n).inv = ((AlgebraicTopology.singularHomologyFunctor C n).obj R).map (TopCat.ofHom e.invFun)