Homotopy invariance of singular homology with local coefficients #
Let H be a homotopy from f : X ⟶ Y to g : X ⟶ Y and let L be a local coefficient system
on Y. The two maps induced on twisted singular chains start from different coefficient systems,
f⁎L and g⁎L, which LocalCoefficientSystem.pullbackHomotopyIso identifies by transport along
the paths t ↦ H (t, x). This file shows that after this identification the two maps are chain
homotopic (TopCat.Homotopy.twistedChainComplexHomotopy), so that they agree on twisted homology
(TopCat.Homotopy.twistedHomologyMap_eq_comp).
This is the homotopy axiom for homology with local coefficients. The cohomological form is in
TauCeti.AlgebraicTopology.Cohomology.Twisted.HomotopyInvariance. As a consequence, a homotopy
equivalence e : X ≃ₕ Y induces isomorphisms H_k(X; e⁎L) ≅ H_k(Y; L) for every local
coefficient system L on Y (ContinuousMap.HomotopyEquiv.isIso_twistedHomologyMap).
Main declarations #
TopCat.Homotopy.twistedChainsHomotopy: the simplicial homotopy of twisted chains.TopCat.Homotopy.twistedChainComplexHomotopy: the chain homotopy of twisted chain complexes.TopCat.Homotopy.twistedHomologyMap_eq_comp: homotopic maps induce the same map on twisted homology, up to the identification of the two pullback systems.ContinuousMap.HomotopyEquiv.isIso_twistedHomologyMap,ContinuousMap.HomotopyEquiv.quasiIso_twistedChainComplexMap: a homotopy equivalence induces isomorphisms on twisted homology.
Implementation notes #
The argument follows Mathlib's proof of homotopy invariance of untwisted singular homology by
F. Odermatt and J. Riou (TopCat.Homotopy.singularChainComplexFunctorObjMap in
Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean, which goes through
SSet.Homotopy.chainComplexMap and SimplicialObject.Homotopy.sSetChainComplexMap in
Mathlib/AlgebraicTopology/SimplicialSet/Homology/HomotopyInvariance.lean), with coefficients in
a local coefficient system. As there, the chain homotopy is obtained from a simplicial homotopy by
Mathlib's SimplicialObject.Homotopy.toChainHomotopy (F. Odermatt), here through
SimplicialObject.Homotopy.toTwistedChainComplexHomotopy.
The chain homotopy comes from a simplicial homotopy of twisted chains, which lifts the
combinatorial homotopy H.toSSet.toSimplicialObjectHomotopy of singular simplicial sets, obtained
from TopCat.Homotopy.toSSet by Mathlib's SSet.Homotopy.toSimplicialObjectHomotopy (J. Riou).
That homotopy sends a singular simplex σ of X to simplices h i σ of Y which start at the
image under f of the initial vertex of σ, so the coefficients of σ are carried to those of
h i σ without transport. The simplicial identities then reduce to the identities of the
combinatorial homotopy, except where the zeroth face moves the initial vertex. There the
coefficient transport runs along the first edge of h i σ: for i ≥ 1 this edge is the image
under f of the first edge of σ, and for i = 0 it is the path traced by H at the initial
vertex of σ (TopCat.Homotopy.pathTransport_toSimplicialObjectHomotopy_h_zero_heq), which is
the transport that defines the identification of f⁎L with g⁎L.
References #
- A. Hatcher, Algebraic Topology, Section 3.H, for homotopy invariance of homology with local coefficients.
- J. P. May, Simplicial Objects in Algebraic Topology, Chapter I, for simplicial homotopies.
The simplices of the combinatorial homotopy extracted from a homotopy H are obtained by
evaluating H on a degeneracy of the given simplex and on a parametrization of the unit
interval.
The combinatorial homotopy extracted from a homotopy H from f to g starts every simplex
at the image under f of its initial vertex.
The first edge of the image of a vertex y under the combinatorial homotopy extracted from a
homotopy H runs along the path t ↦ H (t, y).
On the summand of a simplex σ with at least one edge, the transport along the zeroth face of
the simplex h (j + 1) σ of the combinatorial homotopy is the image under f of the transport
along the zeroth face of σ.
On the summand of a simplex σ, the transport along the zeroth face of the simplex h 0 σ of
the combinatorial homotopy is transport along the path traced by H at the initial vertex of
σ.
The coefficient module of the pullback system at the initial vertex of a simplex is the coefficient module at the initial vertex of its image under the combinatorial homotopy.
A homotopy H from f to g induces a simplicial homotopy from the morphism of twisted
chains induced by f to the morphism induced by g, preceded by the identification of the
pullback systems along H. It sends the summand of a simplex σ identically onto the summand of
the simplex h i σ of the combinatorial homotopy H.toSSet.toSimplicialObjectHomotopy.
Instances For
The simplicial homotopy of twisted chains sends the summand of a simplex σ identically onto
the summand of the simplex h i σ of the combinatorial homotopy.
The simplicial homotopy of twisted chains sends the summand of a simplex σ identically onto
the summand of the simplex h i σ of the combinatorial homotopy.
A homotopy H from f to g induces a chain homotopy from the map of twisted chain
complexes induced by f to the map induced by g, preceded by the identification of the pullback
systems along H.
Instances For
The twisted prism homotopy is the alternating simplicial prism operator under the canonical identifications of twisted chains with the alternating face map complex.
Homotopy invariance of homology with local coefficients: homotopic maps induce the same map on twisted singular homology, after the identification of the two pullback systems by transport along the homotopy.
A homotopy equivalence induces isomorphisms on singular homology with local
coefficients: for a homotopy equivalence e : X ≃ₕ Y and a local coefficient system L on Y,
the map H_k(X; e⁎L) ⟶ H_k(Y; L) is an isomorphism.
A homotopy equivalence induces a quasi-isomorphism of singular chains with local coefficients.