Relative homology vanishes below the connectivity of a pair

Let A be a subspace of X such that every point of X is joined by a path to A and the relative homotopy sets πₖ(X, A, a) are trivial for 0 < k < n and every a ∈ A. Then the relative singular homology Hₘ(X, A; R) vanishes for every m < n and every coefficient ring R (TauCeti.isZero_singularHomology_ofSubset_of_relHomotopyGroup). This is the vanishing half of the relative Hurewicz theorem; unlike the isomorphism in degree n, it needs no assumption on the fundamental groups of X and A.

The proof is Eilenberg's deformation of singular chains, as for the absolute case TauCeti.isZero_singularHomologyFunctor_of_subsingleton_homotopyGroup. By the compression lemma the singular cubes of X deform into A below dimension n (TauCeti.nonempty_subspaceCubeDeformation_of_relHomotopyGroup). The end of such a deformation D is a chain endomorphism D.endChainMap R of the normalized cubical chains of X, chain homotopic to the identity through the swept-cube operator. It fixes the chains of A, and the swept-cube operator kills them, because the deformation of a cube of A is constant. So the homotopy descends to the relative cubical chains of (X, A). There the end of the deformation vanishes in every degree m < n, since it carries every cube of dimension m into A. Hence the identity of the relative cubical homology in degree m is zero (TauCeti.SubspaceCubeDeformation.isZero_homology_cubicalChainComplex), and the comparison of relative cubical and simplicial chains transports this to relative singular homology.

The long exact sequence of the pair then gives the range in which the inclusion of A sees the homology of X: Hₘ(A; R) ⟶ Hₘ(X; R) is surjective for m < n (TauCeti.epi_singularHomologyMap_subtypeVal_of_relHomotopyGroup) and bijective for m + 1 < n (TauCeti.isIso_singularHomologyMap_subtypeVal_of_relHomotopyGroup_of_add_one_lt).

Main results

• TauCeti.SubspaceCubeDeformation.relEndHomotopy: the chain homotopy from the identity to the end of the deformation, on the relative cubical chains of (X, A).
• TauCeti.SubspaceCubeDeformation.isZero_homology_cubicalChainComplex: relative cubical homology vanishes below the dimension bound of a deformation into A.
• TauCeti.SubspaceCubeDeformation.homologyπ_mem_of_cube: in positive degrees at most that bound, relative cubical homology is generated by the classes of single cubes sending the boundary of the cube into A.
• TauCeti.isZero_singularHomology_ofSubset_of_relHomotopyGroup: relative singular homology vanishes below the connectivity of the pair.
• TauCeti.epi_singularHomologyMap_subtypeVal_of_relHomotopyGroup, TauCeti.isIso_singularHomologyMap_subtypeVal_of_relHomotopyGroup_of_add_one_lt: the inclusion of the subspace is surjective on homology below the connectivity of the pair, and bijective one degree lower.

References

• S. Eilenberg, Singular homology theory, Ann. of Math. (2) 45 (1944), 407–447, for the deformation of the singular chains of a pair into those of the subspace.
• A. Hatcher, Algebraic Topology, Section 4.1, Lemma 4.6 (the compression lemma), and Section 4.2, Theorem 4.32 (the relative Hurewicz theorem).

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplex_map_comp_endChainMap {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] : CategoryTheory.CategoryStruct.comp ((normalizedCubicalChainComplex R).map TopPair.map) (D.endChainMap R) = (normalizedCubicalChainComplex R).map TopPair.map

The end of a deformation into the subspace of a pair fixes the chains of the subspace, as chain maps.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplex_map_comp_endChainMap_assoc {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] {Z : ChainComplex (ModuleCat R) ℕ} (h : (normalizedCubicalChainComplex R).obj TopPair.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp ((normalizedCubicalChainComplex R).map TopPair.map) (CategoryTheory.CategoryStruct.comp (D.endChainMap R) h) = CategoryTheory.CategoryStruct.comp ((normalizedCubicalChainComplex R).map TopPair.map) h

The end of a deformation into the subspace of a pair fixes the chains of the subspace, as chain maps.

noncomputable def TauCeti.SubspaceCubeDeformation.relEndChainMap {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] : TopPair.cubicalChainComplex R P ⟶ TopPair.cubicalChainComplex R P

The end of a deformation into the subspace of a pair, on the relative cubical chains of the pair.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.π_relEndChainMap {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((normalizedCubicalChainComplex R).map TopPair.map)) (D.relEndChainMap R) = CategoryTheory.CategoryStruct.comp (D.endChainMap R) (CategoryTheory.Limits.cokernel.π ((normalizedCubicalChainComplex R).map TopPair.map))

@[simp]

theorem TauCeti.SubspaceCubeDeformation.π_relEndChainMap_assoc {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] {Z : ChainComplex (ModuleCat R) ℕ} (h : TopPair.cubicalChainComplex R P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((normalizedCubicalChainComplex R).map TopPair.map)) (CategoryTheory.CategoryStruct.comp (D.relEndChainMap R) h) = CategoryTheory.CategoryStruct.comp (D.endChainMap R) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((normalizedCubicalChainComplex R).map TopPair.map)) h)

noncomputable def TauCeti.SubspaceCubeDeformation.relEndHomotopy {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] : Homotopy (CategoryTheory.CategoryStruct.id (TopPair.cubicalChainComplex R P)) (D.relEndChainMap R)

The chain homotopy from the identity to the end of a deformation into the subspace of a pair, on relative cubical chains, descended from TauCeti.SubspaceCubeDeformation.endHomotopy.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.π_relEndHomotopy_hom {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] (i j : ℕ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.cokernel.π ((normalizedCubicalChainComplex R).map TopPair.map)).f i) ((D.relEndHomotopy R).hom i j) = CategoryTheory.CategoryStruct.comp ((D.endHomotopy R).hom i j) ((CategoryTheory.Limits.cokernel.π ((normalizedCubicalChainComplex R).map TopPair.map)).f j)

The quotient equation for the homotopy operator on relative cubical chains.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.π_relEndHomotopy_hom_assoc {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] (i j : ℕ) {Z : ModuleCat R} (h : (TopPair.cubicalChainComplex R P).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.cokernel.π ((normalizedCubicalChainComplex R).map TopPair.map)).f i) (CategoryTheory.CategoryStruct.comp ((D.relEndHomotopy R).hom i j) h) = CategoryTheory.CategoryStruct.comp ((D.endHomotopy R).hom i j) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.cokernel.π ((normalizedCubicalChainComplex R).map TopPair.map)).f j) h)

The quotient equation for the homotopy operator on relative cubical chains.

theorem TauCeti.SubspaceCubeDeformation.relEndChainMap_f_eq_zero {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] {m : ℕ} (hm : ↑m < n) : (D.relEndChainMap R).f m = 0

Below dimension n, the end of a deformation into the subspace vanishes on relative cubical chains: it carries every cube into the subspace.

theorem TauCeti.SubspaceCubeDeformation.isZero_homology_cubicalChainComplex {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] {m : ℕ} (hm : ↑m < n) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (TopPair.cubicalChainComplex R P) m)

Relative cubical homology vanishes below the dimension bound of a deformation into the subspace: if the singular cubes of X deform into A below dimension n, then the relative normalized cubical homology of (X, A) vanishes in every degree m < n.

theorem TauCeti.SubspaceCubeDeformation.isZero_singularHomology {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] {m : ℕ} (hm : ↑m < n) : CategoryTheory.Limits.IsZero (P.singularHomology (↧R) m)

Relative singular homology vanishes below the dimension bound of a deformation into the subspace.

theorem TauCeti.SubspaceCubeDeformation.homologyπ_mem_of_cube {P : TopPair} {n : ℕ∞} (D : SubspaceCubeDeformation (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) n) (R : Type u) [Ring R] {m : ℕ} (hm : ↑m < n) (T : Submodule R ↑(HomologicalComplex.homology (TopPair.cubicalChainComplex R P) (m + 1))) (hT : ∀ (c : SingularCube (↑TopPair.fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map))), (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex R P) (m + 1))) (TopPair.cubicalCycleOfCube R c hc) ∈ T) (z : ↑(HomologicalComplex.cycles (TopPair.cubicalChainComplex R P) (m + 1))) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex R P) (m + 1))) z ∈ T

Relative cubical homology in positive degrees at most the dimension bound is generated by single cubes. If the singular cubes of X deform into A below dimension n and m < n, then every submodule of the relative normalized cubical homology H^□ₘ₊₁(X, A) containing the classes of all singular (m + 1)-cubes sending the boundary of the cube into A is everything.

theorem TauCeti.isZero_singularHomology_ofSubset_of_relHomotopyGroup {X : TopCat} {A : Set ↑X} {n : ℕ} (h₀ : ∀ (x : ↑X), ∃ a ∈ A, Joined x a) (h : ∀ (k : ℕ), k + 1 < n → ∀ (a : ↑A), Subsingleton (RelHomotopyGroup (Fin k) { pair := TopPair.ofSubset A, basepoint := a })) (R : Type u) [Ring R] {m : ℕ} (hm : m < n) : CategoryTheory.Limits.IsZero ((TopPair.ofSubset A).singularHomology (↧R) m)

Relative singular homology vanishes below the connectivity of the pair. If every point of X is joined by a path to a point of A, and the relative homotopy set π_{k+1}(X, A, a) is trivial for every k + 1 < n and every a ∈ A, then Hₘ(X, A; R) = 0 for every m < n and every coefficient ring R.

theorem TauCeti.epi_singularHomologyMap_subtypeVal_of_relHomotopyGroup {X : TopCat} {A : Set ↑X} {n : ℕ} (h₀ : ∀ (x : ↑X), ∃ a ∈ A, Joined x a) (h : ∀ (k : ℕ), k + 1 < n → ∀ (a : ↑A), Subsingleton (RelHomotopyGroup (Fin k) { pair := TopPair.ofSubset A, basepoint := a })) (R : Type u) [Ring R] {m : ℕ} (hm : m < n) : CategoryTheory.Epi (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) m).obj ↧R).map (TopCat.ofHom (ContinuousMap.subtypeVal A)))

The inclusion of a subspace induces surjections on homology below the connectivity of the pair. If every point of X is joined by a path to a point of A, and the relative homotopy set π_{k+1}(X, A, a) is trivial for every k + 1 < n and every a ∈ A, then the inclusion of A into X induces an epimorphism Hₘ(A; R) ⟶ Hₘ(X; R) for every m < n and every coefficient ring R.

theorem TauCeti.isIso_singularHomologyMap_subtypeVal_of_relHomotopyGroup_of_add_one_lt {X : TopCat} {A : Set ↑X} {n : ℕ} (h₀ : ∀ (x : ↑X), ∃ a ∈ A, Joined x a) (h : ∀ (k : ℕ), k + 1 < n → ∀ (a : ↑A), Subsingleton (RelHomotopyGroup (Fin k) { pair := TopPair.ofSubset A, basepoint := a })) (R : Type u) [Ring R] {m : ℕ} (hm : m + 1 < n) : CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) m).obj ↧R).map (TopCat.ofHom (ContinuousMap.subtypeVal A)))

The inclusion of a subspace induces isomorphisms on homology below the connectivity of the pair minus one. If every point of X is joined by a path to a point of A, and the relative homotopy set π_{k+1}(X, A, a) is trivial for every k + 1 < n and every a ∈ A, then the inclusion of A into X induces an isomorphism Hₘ(A; R) ≅ Hₘ(X; R) for every m + 1 < n and every coefficient ring R. Together with TauCeti.epi_singularHomologyMap_subtypeVal_of_relHomotopyGroup in degree m = n - 1, this is the range given by the long exact sequence of the pair.