Homotopy invariance of singular homology

Stream: homology

[Fabian Odermatt]

Hi

I’m considering proving homotopy invariance of singular homology using Brendan Murphy’s work as a blueprint, porting as much as possible. Since mathlib has changed quite significantly since then, I would like to hear your opinions on whether this approach is still a good fit for mathlib. What I have in mind is that algebraic topology in mathlib is now built on top of fairly general category theory, which could in principle give more general statements than Brendan’s original proof.

Specifically, his proof relies on the usual free‑$R$‑module structure on singular chains, with singular simplices as basis elements. So I would state homotopy invariance for singular homology with coefficients in a commutative ring $R$, i.e. with target ModuleCat R.

variable (R : Type) [CommRing R]
variable {X Y : TopCat} (f g : X ⟶ Y) (n : ℕ)

theorem singularHomology_map_eq_of_homotopy
    (H : ContinuousMap.Homotopy f.hom g.hom) :
    (((singularHomologyFunctor (ModuleCat R) n).obj (ModuleCat.of R R))).map f =
    (((singularHomologyFunctor (ModuleCat R) n).obj (ModuleCat.of R R))).map g :=

In addition, he uses an acyclic models theorem which (roughly) says that if two natural transformations $α, β : F ⟶ G$ have the same effect on $H_0$ on a family of model objects, and $G$ is acyclic on these models, then $α$ and $β$ are naturally chain‑homotopic. I’m not that deep into category theory yet, so I don’t fully understand all of this, but since this part of the proof is relatively self‑contained, I’m hoping it should be possible to reprove an appropriate version in mathlib4 as well.

There are obviously more technical details in the proof that might cause problems, but my plan would be to start and address issues as they arise. I know there have been previous attempts to port Brendan’s Brouwer proof; if anyone knows what specific obstacles came up there, I would be very interested to hear about them.

So, my main question is whether the statement above is general enough for mathlib or if you want to stick to the category-theory approach.

I feel like it is useful to make progress on singular homology and reach some standard theorems, even if this currently means using more geometric, less obviously “optimal” categorical proofs. I also don't know if there are "categorical" proofs of excision, but if not, going down to the geometric level would be necessary at some point anyway.

[Joël Riou]

For the homotopy invariance, I feel it would be better to show that if f and g are homotopic morphisms of simplicial sets, then the corresponding morphisms of chain complexes (after applying SSet.singularChainComplexFunctor) are homotopic. The similar result you mention for homotopies between continuous maps of topological spaces follows easily as the singular homology of a topological space X is obtained by taking the homology of the singular simplicial set of X (whose n-simplices are continuous maps from the standard topological n-simplex to X).
The strategy of proof may combine two steps:

1. show the result using the combinatorial definition of homotopies between morphisms of simplicial objects https://ncatlab.org/nlab/show/simplicial+homotopy;
2. relate the combinatorial definition of homotopies with the data of a morphism X ⊗ Δ[1] ⟶ Y.

(I am in the process of adding results about the simplicial sets Δ[p] ⊗ Δ[q] in #32237, and soon there will be some specialized versions for Δ[n] ⊗ Δ[1] which should be relevant for 2. If you work on 1., the combination of both should lead to the expected homotopy invariance result.)

[Fabian Odermatt]

I'll have a look into it

[Fabian Odermatt]

So I think I managed to define simplicial homotopy as on the nlab page. See PR #32881.
Currently, I'm trying to construct a chain homotopy between the induced morphisms on the alternating face map complexes, given a simplicial homotopy.

def SimplicialHomotopy.toChainHomotopy (H : SimplicialHomotopy f g) :
    Homotopy
      ((alternatingFaceMapComplex C).map f)
      ((alternatingFaceMapComplex C).map g) := by sorry

which will give the corollary

theorem SimplicialHomotopy.map_homology_eq
    [CategoryWithHomology C] (H : SimplicialHomotopy f g) (n : ℕ) :
    (HomologicalComplex.homologyFunctor C _ n).map
        ((alternatingFaceMapComplex C).map f) =
    (HomologicalComplex.homologyFunctor C _ n).map
        ((alternatingFaceMapComplex C).map g) := by
  simpa using (H.toChainHomotopy).homologyMap_eq n

This should then give the result aswell for SimplicialSets, right?

Would you mind explaining in a bit more detail the step 2. of your plan? Or hint to some places where I could read about that. Thank you!

[Joël Riou]

As a complement to your definition in #32881, you could show that SimplicialHomotopy behaves well with respect to the postcomposition with a functor C ⥤ D (SimplicialObject.whiskering). In addition to the construction of a homotopy between the actions on alternating face map complexes, this should give that if f and g are maps of simplicial sets that are homotopic in the sense of SimplicialHomotopy, then the induced morphisms on the complexes which compute the singular homology are chain homotopic.
Two things would remain:

• A homotopy in the sense of the data of a map X ⊗ Δ[1] ⟶ Y is the same as SimplicialHomotopy (possibly up to switching f and g?). For the homotopy invariance, we need only one direction. Details may become easier after I have made a few more pull requests;
• When we have a continuous map X x [0, 1] ⟶ Y between topological spaces, one may apply the singular simplicial set functor, which commutes with products, so that we should get an homotopy Sing X ⊗ Δ[1] ⟶ Sing Y by using a suitable 1-simplex of Sing [0, 1].

I would suggest you continue working on the homotopy on the alternating chain map complex. The chain homotopy should be given by the alternating sum of the maps h (up to a sign), see p. 13 of Simplicial objects in algebraic topology by J. Peter May for similar material.

[Joël Riou]

I have added some suggestions to #32881. In order to be reasonably sure that the equations are correct (in the sense that the translation from ncatlab is correct, and that there is no typo in this reference!), it would be good to wait for the formalisation of the chain homotopy on alternating face map complexes.
(Also, in the unfortunate case the chain homotopy on the alternating face map complexes may require an extra sign, we may want to switch the roles of f and g in the definition of SimplicialHomotopy.)

[Fabian Odermatt]

Perfect, yes I agree