Homotopy invariance of singular cohomology

Singular cochains are obtained from singular chains by applying Hom(-, M), and an additive functor carries chain homotopies to chain homotopies. So the chain homotopy that a homotopy of maps induces on singular chains gives a cochain homotopy on singular cochains, and homotopic maps induce the same map on singular cohomology. Maps that are inverse to each other up to homotopy therefore induce isomorphisms on singular cohomology. This is the homotopy axiom of Eilenberg--Steenrod for the singular cohomology theory, in both its absolute and its relative form. The chain homotopies it is deduced from are Mathlib's SSet.Homotopy.chainComplexMap, applied to the simplicial homotopy TopCat.Homotopy.toSSet, for a space, and TopPair.Homotopy.singularChainComplexMap for a pair. The homology counterparts of the results below are Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean (F. Odermatt, J. Riou) for a space and TauCeti/AlgebraicTopology/Singular/Homotopy/Invariance.lean for a pair.

Main results

• TopCat.Homotopy.singularCochainComplexMap and TopPair.Homotopy.singularCochainComplexMap: the cochain homotopy induced by a homotopy of maps of spaces, respectively of pairs.
• TopCat.Homotopy.congr_singularCohomologyMap and TopPair.Homotopy.congr_singularCohomologyMap: homotopic maps induce the same map on singular cohomology.
• TopCat.isIso_singularCohomologyMap and TopPair.isIso_singularCohomologyMap: a map with a homotopy inverse induces an isomorphism on singular cohomology.

References

• A. Hatcher, Algebraic Topology, Section 3.1.
• S. Eilenberg and N. Steenrod, Foundations of Algebraic Topology, Chapter VII.

noncomputable def TopCat.Homotopy.singularCochainComplexMap {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : _root_.Homotopy (TopCat.singularCochainComplexMap f) (TopCat.singularCochainComplexMap g)

A homotopy between continuous maps induces a cochain homotopy between the induced maps of singular cochain complexes.

Equations

• H.singularCochainComplexMap R k M = Homotopy.linearYonedaFunctorMap k M (H.toSSet.chainComplexMap R)

@[simp]

theorem TopCat.Homotopy.singularCochainComplexMap_hom_apply {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (p q : ℕ) (x : ↑((singularCochainComplex R k M Y).X p)) : (CategoryTheory.ConcreteCategory.hom ((H.singularCochainComplexMap R k M).hom p q)) x = CategoryTheory.CategoryStruct.comp ((H.toSSet.chainComplexMap R).hom q p) x

The cochain homotopy induced by a homotopy of continuous maps is precomposition with the chain homotopy it induces on singular chains.

theorem TopCat.Homotopy.congr_singularCohomologyMap {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : TopCat.singularCohomologyMap f n = TopCat.singularCohomologyMap g n

Homotopic continuous maps induce the same map on singular cohomology.

theorem TopCat.isIso_singularCohomologyMap {X Y : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (f : X ⟶ Y) (f' : Y ⟶ X) (H : Homotopy (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.id X)) (H' : Homotopy (CategoryTheory.CategoryStruct.comp f' f) (CategoryTheory.CategoryStruct.id Y)) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : CategoryTheory.IsIso (TopCat.singularCohomologyMap f n)

Continuous maps which are inverse to each other up to homotopy induce isomorphisms on singular cohomology.

noncomputable def TopPair.Homotopy.singularCochainComplexMap {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : _root_.Homotopy (TopPair.singularCochainComplexMap f) (TopPair.singularCochainComplexMap g)

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

Equations

• H.singularCochainComplexMap R k M = Homotopy.linearYonedaFunctorMap k M (H.singularChainComplexMap R)

@[simp]

theorem TopPair.Homotopy.singularCochainComplexMap_hom_apply {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (p q : ℕ) (x : ↑((P'.singularCochainComplex R k M).X p)) : (CategoryTheory.ConcreteCategory.hom ((H.singularCochainComplexMap R k M).hom p q)) x = CategoryTheory.CategoryStruct.comp ((H.singularChainComplexMap R).hom q p) x

The cochain homotopy induced by a homotopy of maps of pairs is precomposition with the chain homotopy it induces on relative singular chains.

theorem TopPair.Homotopy.congr_singularCohomologyMap {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : TopPair.singularCohomologyMap f n = TopPair.singularCohomologyMap g n

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

theorem TopPair.isIso_singularCohomologyMap {P P' : TopPair} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian 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) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : CategoryTheory.IsIso (TopPair.singularCohomologyMap f n)

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