Compression of cubical chains with local coefficients

Let D be a TauCeti.SubspaceCubeDeformation A ⊤: a deformation of every singular cube of X into a subspace A, compatible with faces and degeneracies and fixing the cubes of A. For every local coefficient system L on X, this file shows that the inclusion of A induces a chain homotopy equivalence from the normalized cubical chains of A with coefficients in the restriction of L to the normalized cubical chains of X with coefficients in L. This is the local-coefficient form of TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplexHomotopyEquiv.

A coefficient of a cube lives in the fibre of L at the origin of the cube, so the operators of the constant case have to move it.

• During the deformation, the origin of a cube c traces a path from c 0 to the origin of the end D.retract c of the deformation. Its class is D.originTransport c. The retraction D.twistedRetractChain L sends c with a coefficient a to D.retract c with a transported along this path. It is a chain map, and a left inverse of the inclusion.
• The swept cube D.sweep c starts at the origin of c, so the swept-cube operator D.twistedPrismChain L keeps the coefficient. Every transport that occurs in the faces of the swept cube, in the retraction and in the faces of c is a path class inside the swept cube. The cube is simply connected, so such a path class is determined by its end points. Hence the prism identity ∂ P + P ∂ = ι ρ - id holds exactly as for constant coefficients.

By the compression lemma such a deformation exists as soon as every point of X is joined by a path to A and all relative homotopy sets π_{n+1}(X, A, a) vanish (TauCeti.quasiIso_normalizedTwistedCubicalChainComplexMap_subtypeVal_of_relHomotopyGroup). For the inclusion of the bottom face of the mapping cylinder of a weak homotopy equivalence, this is the main step in the proof that weak homotopy equivalences induce isomorphisms on homology with local coefficients.

Main definitions

• TauCeti.SubspaceCubeDeformation.originTransport: the class of the path traced by the origin of a cube during its deformation.
• TauCeti.SubspaceCubeDeformation.twistedRetractChain, TauCeti.SubspaceCubeDeformation.twistedPrismChain: the retraction and the swept-cube operator on normalized cubical chains with local coefficients.
• TauCeti.SubspaceCubeDeformation.twistedRetractChainMap, TauCeti.SubspaceCubeDeformation.twistedRetractHomotopy: the retraction as a chain map, and the chain homotopy from the identity to its composite with the inclusion.
• TauCeti.SubspaceCubeDeformation.normalizedTwistedCubicalChainComplexHomotopyEquiv: the chain homotopy equivalence induced by the inclusion of A.

Main results

• TauCeti.SubspaceCubeDeformation.twistedRetractChain_map_subtypeVal: the retraction is a left inverse of the inclusion.
• TauCeti.SubspaceCubeDeformation.boundary_twistedPrismChain_add_twistedPrismChain_boundary: the prism identity ∂ P + P ∂ = ι ρ - id.
• TauCeti.SubspaceCubeDeformation.quasiIso_normalizedTwistedCubicalChainComplexMap: the inclusion of A induces a quasi-isomorphism of normalized cubical chains with local coefficients.
• TauCeti.quasiIso_normalizedTwistedCubicalChainComplexMap_subtypeVal_of_relHomotopyGroup: the same conclusion from the vanishing of the relative homotopy sets.

References

• The chain-level construction extends the constant-coefficient one of TauCeti.AlgebraicTopology.Singular.Cubical.Compression.Retraction.
• A. Hatcher, Algebraic Topology, Section 3.H (homology with local coefficients) and Section 4.1, Proposition 4.21 (a weak homotopy equivalence induces isomorphisms on homology).
• J.-P. Serre, Homologie singulière des espaces fibrés. Applications, Ann. of Math. 54 (1951), Chapter II, for cubical chains with local coefficients.
• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II, for normalized cubical chains and their prism operators.

def TauCeti.SubspaceCubeDeformation.originTransport {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube X m) : { as := c 0 } ⟶ { as := ↑((D.retract c) 0) }

The transport along the track of the origin of the singular cube c: the class of the path traced by the origin of c during its deformation into A.

theorem TauCeti.SubspaceCubeDeformation.originTransport_heq {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube X m) : D.originTransport c ≍ ContinuousMap.pathClass (D.sweep c) 0 (Fin.cons 1 0)

The transport along the track of the origin of c is the path class inside the swept cube of c from its origin to the origin of the end of the deformation.

theorem TauCeti.SubspaceCubeDeformation.originTransport_comp_pathClass_heq {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) : CategoryTheory.CategoryStruct.comp (D.originTransport c) (((ContinuousMap.subtypeVal A).comp (D.retract c)).pathClass 0 ((SingularCube.face i t (ContinuousMap.id (Fin (m + 1) → ↑unitInterval))) 0)) ≍ CategoryTheory.CategoryStruct.comp (ContinuousMap.pathClass c 0 ((SingularCube.face i t (ContinuousMap.id (Fin (m + 1) → ↑unitInterval))) 0)) (D.originTransport (ContinuousMap.comp c (SingularCube.face i t (ContinuousMap.id (Fin (m + 1) → ↑unitInterval)))))

Transport along the track of the origin of c, followed by transport inside the end of the deformation into one of its faces, is transport inside c into that face followed by transport along the track of the origin of the face.

theorem TauCeti.SubspaceCubeDeformation.originTransport_subtypeVal_comp_heq {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube (↑A) m) : D.originTransport ((ContinuousMap.subtypeVal A).comp c) ≍ CategoryTheory.CategoryStruct.id { as := ↑(c 0) }

The track of the origin of a cube of A is constant.

The operators on unnormalized chains

The operators on normalized chains

noncomputable def TauCeti.SubspaceCubeDeformation.twistedRetractChain {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) (m : ℕ) : L.NormalizedTwistedCubicalChain m →ₗ[R] ((LocalCoefficientSystem.pullback (ContinuousMap.subtypeVal A)).obj L).NormalizedTwistedCubicalChain m

The retraction onto the cubes of A on normalized cubical chains with coefficients in L: the end of the deformation of a cube, carrying the coefficient transported along the track of the origin of the cube, in the restriction of L to A.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.twistedRetractChain_ofCube {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) {m : ℕ} (c : SingularCube (↑X) m) (a : ↑(L.obj { as := c 0 })) : (D.twistedRetractChain L m) ((LocalCoefficientSystem.NormalizedTwistedCubicalChain.ofCube L c) a) = (LocalCoefficientSystem.NormalizedTwistedCubicalChain.ofCube ((LocalCoefficientSystem.pullback (ContinuousMap.subtypeVal A)).obj L) (D.retract c)) ((CategoryTheory.ConcreteCategory.hom (L.map (D.originTransport c))) a)

The retraction sends a cube with a coefficient to the end of the deformation of the cube, with the coefficient transported along the track of the origin.

noncomputable def TauCeti.SubspaceCubeDeformation.twistedPrismChain {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) (m : ℕ) : L.NormalizedTwistedCubicalChain m →ₗ[R] L.NormalizedTwistedCubicalChain (m + 1)

The negative swept-cube operator on normalized cubical chains with coefficients in L.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.twistedPrismChain_ofCube {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) {m : ℕ} (c : SingularCube (↑X) m) (a : ↑(L.obj { as := c 0 })) : (D.twistedPrismChain L m) ((LocalCoefficientSystem.NormalizedTwistedCubicalChain.ofCube L c) a) = -(LocalCoefficientSystem.NormalizedTwistedCubicalChain.ofCube L (D.sweep c)) ((CategoryTheory.ConcreteCategory.hom (L.map (CategoryTheory.eqToHom ⋯))) a)

The swept-cube operator sends a cube with a coefficient to the negative of its swept cube, which starts at the origin of the cube and carries the same coefficient.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.twistedRetractChain_map_subtypeVal {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) {m : ℕ} (g : ((LocalCoefficientSystem.pullback (ContinuousMap.subtypeVal A)).obj L).NormalizedTwistedCubicalChain m) : (D.twistedRetractChain L m) ((LocalCoefficientSystem.NormalizedTwistedCubicalChain.map (ContinuousMap.subtypeVal A) L m) g) = g

The retraction is a left inverse of the inclusion on normalized cubical chains with local coefficients, since the deformation fixes the cubes of A.

theorem TauCeti.SubspaceCubeDeformation.boundary_twistedRetractChain {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) (m : ℕ) (g : L.NormalizedTwistedCubicalChain (m + 1)) : (LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary ((LocalCoefficientSystem.pullback (ContinuousMap.subtypeVal A)).obj L) m) ((D.twistedRetractChain L (m + 1)) g) = (D.twistedRetractChain L m) ((LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary L m) g)

The retraction commutes with the boundary.

theorem TauCeti.SubspaceCubeDeformation.boundary_twistedPrismChain_add_twistedPrismChain_boundary {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) (m : ℕ) (g : L.NormalizedTwistedCubicalChain (m + 1)) : (LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary L (m + 1)) ((D.twistedPrismChain L (m + 1)) g) + (D.twistedPrismChain L m) ((LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary L m) g) = (LocalCoefficientSystem.NormalizedTwistedCubicalChain.map (ContinuousMap.subtypeVal A) L (m + 1)) ((D.twistedRetractChain L (m + 1)) g) - g

The prism identity ∂ P + P ∂ = ι ρ - id in positive degrees, for the swept-cube operator P, the retraction ρ and the inclusion ι of A.

theorem TauCeti.SubspaceCubeDeformation.boundary_twistedPrismChain_zero {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) (g : L.NormalizedTwistedCubicalChain 0) : (LocalCoefficientSystem.NormalizedTwistedCubicalChain.boundary L 0) ((D.twistedPrismChain L 0) g) = (LocalCoefficientSystem.NormalizedTwistedCubicalChain.map (ContinuousMap.subtypeVal A) L 0) ((D.twistedRetractChain L 0) g) - g

The prism identity ∂ P = ι ρ - id in degree zero.

The chain homotopy equivalence of normalized cubical chain complexes

noncomputable def TauCeti.SubspaceCubeDeformation.twistedRetractChainMap {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) : L.normalizedTwistedCubicalChainComplex ⟶ ((LocalCoefficientSystem.pullback (ContinuousMap.subtypeVal A)).obj L).normalizedTwistedCubicalChainComplex

The retraction onto the cubes of A, as a chain map from the normalized cubical chains of X with coefficients in L to those of A with coefficients in the restriction of L.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.twistedRetractChainMap_f {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) (m : ℕ) : (D.twistedRetractChainMap L).f m = ModuleCat.ofHom (D.twistedRetractChain L m)

The components of the retraction chain map.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedTwistedCubicalChainComplexMap_comp_twistedRetractChainMap {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) : CategoryTheory.CategoryStruct.comp (LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap (ContinuousMap.subtypeVal A) L) (D.twistedRetractChainMap L) = CategoryTheory.CategoryStruct.id ((LocalCoefficientSystem.pullback (ContinuousMap.subtypeVal A)).obj L).normalizedTwistedCubicalChainComplex

The retraction chain map is a left inverse of the chain map induced by the inclusion of A.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedTwistedCubicalChainComplexMap_comp_twistedRetractChainMap_assoc {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) {Z : ChainComplex (ModuleCat R) ℕ} (h : ((LocalCoefficientSystem.pullback (ContinuousMap.subtypeVal A)).obj L).normalizedTwistedCubicalChainComplex ⟶ Z) : CategoryTheory.CategoryStruct.comp (LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap (ContinuousMap.subtypeVal A) L) (CategoryTheory.CategoryStruct.comp (D.twistedRetractChainMap L) h) = h

The retraction chain map is a left inverse of the chain map induced by the inclusion of A.

noncomputable def TauCeti.SubspaceCubeDeformation.twistedRetractHomotopy {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) : Homotopy (CategoryTheory.CategoryStruct.id L.normalizedTwistedCubicalChainComplex) (CategoryTheory.CategoryStruct.comp (D.twistedRetractChainMap L) (LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap (ContinuousMap.subtypeVal A) L))

The chain homotopy from the identity to the composite of the retraction and the inclusion of A, given in degree m by the swept-cube operator -D.twistedPrismChain L m.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.twistedRetractHomotopy_hom_succ {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) (m : ℕ) (g : L.NormalizedTwistedCubicalChain m) : (CategoryTheory.ConcreteCategory.hom ((D.twistedRetractHomotopy L).hom m (m + 1))) g = -(D.twistedPrismChain L m) g

The chain homotopy is the swept-cube operator.

noncomputable def TauCeti.SubspaceCubeDeformation.normalizedTwistedCubicalChainComplexHomotopyEquiv {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) : HomotopyEquiv ((LocalCoefficientSystem.pullback (ContinuousMap.subtypeVal A)).obj L).normalizedTwistedCubicalChainComplex L.normalizedTwistedCubicalChainComplex

The inclusion of A induces a chain homotopy equivalence of normalized cubical chains with local coefficients, from the chains of A with coefficients in the restriction of L to the chains of X with coefficients in L, with the retraction as homotopy inverse.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedTwistedCubicalChainComplexHomotopyEquiv_hom {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) : (D.normalizedTwistedCubicalChainComplexHomotopyEquiv L).hom = LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap (ContinuousMap.subtypeVal A) L

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedTwistedCubicalChainComplexHomotopyEquiv_inv {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (L : LocalCoefficientSystem R X) : (D.normalizedTwistedCubicalChainComplexHomotopyEquiv L).inv = D.twistedRetractChainMap L

theorem TauCeti.SubspaceCubeDeformation.quasiIso_normalizedTwistedCubicalChainComplexMap {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (L : LocalCoefficientSystem R X) (D : SubspaceCubeDeformation A ⊤) : QuasiIso (LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap (ContinuousMap.subtypeVal A) L)

The inclusion of A induces a quasi-isomorphism of normalized cubical chains with local coefficients.

theorem TauCeti.quasiIso_normalizedTwistedCubicalChainComplexMap_subtypeVal_of_relHomotopyGroup {R : Type u} [Ring R] {X : TopCat} {A : Set ↑X} (h₀ : ∀ (x : ↑X), ∃ a ∈ A, Joined x a) (h : ∀ (n : ℕ) (a : ↑A), Subsingleton (RelHomotopyGroup (Fin n) { pair := TopPair.ofSubset A, basepoint := a })) (L : LocalCoefficientSystem R X) : QuasiIso (LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap (ContinuousMap.subtypeVal A) L)

The inclusion of a subspace with vanishing relative homotopy sets induces a quasi-isomorphism of normalized cubical chains with local coefficients. If every point of X is joined by a path to a point of A, and the relative homotopy set π_{n+1}(X, A, a) is trivial for every n and every a ∈ A, then for every local coefficient system L on X the inclusion of A induces isomorphisms H_n(A; L|_A) ≅ H_n(X; L) on normalized cubical homology with local coefficients.