Documentation

TauCeti.AlgebraicTopology.Singular.Homotopy.ConnectedMap

n-connected maps and singular homology #

An n-connected map f : X → Y (ContinuousMap.IsNConnected) induces isomorphisms H_m(X; R) ≅ H_m(Y; R) on singular homology for every m < n, and a surjection in degree n, for every coefficient ring R. This is the range version of the fact that a weak homotopy equivalence induces isomorphisms on homology (ContinuousMap.IsWeakHomotopyEquivalence.isIso_singularHomologyMap), which is the case of maps that are n-connected for every n. No CW structure on X or Y is needed.

The proof factors f through its mapping cylinder M_f as

X ≃ₜ (bottom face of M_f) ↪ M_f → Y.

The first map is a homeomorphism and the last a homotopy equivalence, so both induce isomorphisms on homology. For the middle one, the relative homotopy groups π_{k+1}(M_f, X) vanish for k < n (ContinuousMap.IsNConnected.subsingleton_relHomotopyGroup_mappingCylinder), so the singular cubes of M_f deform into the bottom face below dimension n + 1 and the relative homology H_m(M_f, X; R) vanishes for m ≤ n (ContinuousMap.IsNConnected.isZero_singularHomology_mappingCylinder). The long exact sequence of the pair gives the stated range.

For the inclusion of the n-skeleton of a relative CW complex, which is n-connected (TauCeti.isNConnected_inclusion_skeletonLT), this gives surjectivity on homology in degree n. The isomorphisms below degree n are the classical statement that the skeleton carries the homology of the complex (Hatcher, Lemma 2.34(c)), already available as TauCeti.isIso_homologyMap_skeletonBasePairToComplex_fst.

Main results #

References #

source
theorem ContinuousMap.IsNConnected.isZero_singularHomology_mappingCylinder {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {n : ℕ} (R : Type u) [Ring R] (hf : f.IsNConnected n) {m : ℕ} (hm : m ≤ n) :
CategoryTheory.Limits.IsZero ((TopPair.ofSubset (Set.range ⇑(TauCeti.MappingCylinder.incl f))).singularHomology (↧R) m)

The mapping cylinder of an n-connected map is homologically n-connected relative to its bottom face: if f : X → Y is n-connected, then H_m(M_f, X; R) = 0 for every m ≤ n, where X is identified with the bottom face of the mapping cylinder M_f.

source
theorem ContinuousMap.IsNConnected.isIso_singularHomologyMap {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {n : ℕ} (R : Type u) [Ring R] (hf : f.IsNConnected n) {m : ℕ} (hm : m < n) :
CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) m).obj ↧R).map (TopCat.ofHom f))

An n-connected map induces isomorphisms on singular homology below degree n: if f : X → Y is n-connected, then f_* : H_m(X; R) → H_m(Y; R) is an isomorphism for every m < n and every coefficient ring R.

source
theorem ContinuousMap.IsNConnected.epi_singularHomologyMap {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {n : ℕ} (R : Type u) [Ring R] (hf : f.IsNConnected n) {m : ℕ} (hm : m ≤ n) :
CategoryTheory.Epi (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) m).obj ↧R).map (TopCat.ofHom f))

An n-connected map induces surjections on singular homology up to degree n: if f : X → Y is n-connected, then f_* : H_m(X; R) → H_m(Y; R) is an epimorphism for every m ≤ n and every coefficient ring R.

source
theorem TauCeti.epi_singularHomologyMap_inclusion_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set X} (R : Type u) [Ring R] (hA : ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1)) = A) (hAC : A ⊆ C) {m : ℕ} (hm : m ≤ n) :
CategoryTheory.Epi (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) m).obj ↧R).map (TopCat.ofHom (ContinuousMap.inclusion hAC)))

The inclusion of the n-skeleton is surjective on homology up to degree n. If A is the n-skeleton skeletonLT C (n + 1) of a relative CW complex C, then the inclusion A ↪ C induces an epimorphism H_m(A; R) → H_m(C; R) for every m ≤ n.