Hurewicz isomorphisms for loop spaces

Let (X, x) be a pointed space whose homotopy groups π_1, …, π_{n+2} at x vanish. Then the loop space ΩX is (n + 1)-connected, since π_k(ΩX) ≅ π_{k+1}(X) in every degree k, including k = 0. The Hurewicz theorem for ΩX and the loop-space shift therefore identify

H_{n+2}(ΩX; ℤ) ≅ π_{n+3}(X, x).

Applying this to the loop space, if π_2, …, π_{n+3} vanish at x (no condition on π_1), then

H_{n+2}(Ω²X; ℤ) ≅ π_{n+4}(X, x),

so the first nonvanishing higher homotopy group π_k(X, x), k ≥ 4, is the homology of the double loop space in degree k - 2. The case k = 3 is degree-one Hurewicz (TauCeti.MooreLoopSpace.doubleFirstHomologyAddEquiv). This is the homological input for detecting higher homotopy groups through double loop spaces.

Both the fixed-interval loop spaces Ω X x and the Moore loop spaces MooreLoopSpace X x are treated; for the latter the double-loop identification is also stated for normalized cubical chains. The Hurewicz isomorphism used is the cubical one (HomotopyGroup.cubicalHurewiczAddEquiv), transported to simplicial singular homology by the cubical–simplicial comparison.

Main definitions

• TauCeti.pathLoopSpaceHomologyAddEquiv: π_{n+3}(X, x) ≅ H_{n+2}(ΩX; ℤ).
• TauCeti.doubleLoopSpaceHomologyAddEquiv: π_{n+4}(X, x) ≅ H_{n+2}(Ω²X; ℤ).
• TauCeti.MooreLoopSpace.homologyAddEquiv and TauCeti.MooreLoopSpace.doubleHomologyAddEquiv: the same for Moore loops.
• TauCeti.MooreLoopSpace.doubleCubicalHomologyAddEquiv: π_{n+4}(X, x) is the normalized cubical homology H_{n+2}(ΩᴹΩᴹX; ℤ).

References

• A. Hatcher, Algebraic Topology, Theorem 4.32 and §4.1.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, Propositions 5.11 and 6.21.

Fixed-interval loops

noncomputable def TauCeti.pathLoopSpaceHomologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 1) X x)) : Additive (HomotopyGroup.Pi (n + 3) X x) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(LoopSpace X x)) (n + 2))

Hurewicz for loop spaces. If π_{k+1}(X, x) vanishes for every k < n + 2, then the integral homology of the loop space Ω X x in degree n + 2 is H_{n+2}(ΩX; ℤ) ≅ π_{n+3}(X, x).

theorem TauCeti.pathLoopSpaceHomologyAddEquiv_apply {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 1) X x)) (a : Additive (HomotopyGroup.Pi (n + 3) X x)) : (pathLoopSpaceHomologyAddEquiv x n hX) a = (HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv ⋯) (Additive.ofMul ((HomotopyGroup.pathLoopSpaceMulEquiv (n + 1)).symm (Additive.toMul a)))

TauCeti.pathLoopSpaceHomologyAddEquiv is the inverse loop-space shift followed by the Hurewicz isomorphism of the loop space.

noncomputable def TauCeti.doubleLoopSpaceHomologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 2) X x)) : Additive (HomotopyGroup.Pi (n + 4) X x) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(LoopSpace (LoopSpace X x) (Path.refl x))) (n + 2))

Hurewicz for double loop spaces. If π_{k+2}(X, x) vanishes for every k < n + 2, then the integral homology of the double loop space Ω (Ω X x) (Path.refl x) in degree n + 2 is H_{n+2}(Ω²X; ℤ) ≅ π_{n+4}(X, x).

theorem TauCeti.doubleLoopSpaceHomologyAddEquiv_apply {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 2) X x)) (a : Additive (HomotopyGroup.Pi (n + 4) X x)) : (doubleLoopSpaceHomologyAddEquiv x n hX) a = (pathLoopSpaceHomologyAddEquiv (Path.refl x) n ⋯) (Additive.ofMul ((HomotopyGroup.pathLoopSpaceMulEquiv (n + 2)).symm (Additive.toMul a)))

TauCeti.doubleLoopSpaceHomologyAddEquiv is the inverse loop-space shift followed by the Hurewicz identification for the loop space Ω X x.

Moore loops

noncomputable def TauCeti.MooreLoopSpace.homologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 1) X x)) : Additive (HomotopyGroup.Pi (n + 3) X x) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace X x)) (n + 2))

Hurewicz for Moore loop spaces. If π_{k+1}(X, x) vanishes for every k < n + 2, then the integral homology of the Moore loop space in degree n + 2 is H_{n+2}(ΩᴹX; ℤ) ≅ π_{n+3}(X, x).

theorem TauCeti.MooreLoopSpace.homologyAddEquiv_apply {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 1) X x)) (a : Additive (HomotopyGroup.Pi (n + 3) X x)) : (homologyAddEquiv x n hX) a = (HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv ⋯) (Additive.ofMul ((homotopyGroupMulEquiv x (n + 1)).symm (Additive.toMul a)))

TauCeti.MooreLoopSpace.homologyAddEquiv is the inverse Moore loop-space shift followed by the Hurewicz isomorphism of the Moore loop space.

noncomputable def TauCeti.MooreLoopSpace.doubleHomologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 2) X x)) : Additive (HomotopyGroup.Pi (n + 4) X x) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) (n + 2))

Hurewicz for double Moore loop spaces. If π_{k+2}(X, x) vanishes for every k < n + 2, then the integral homology of the double Moore loop space in degree n + 2 is H_{n+2}(ΩᴹΩᴹX; ℤ) ≅ π_{n+4}(X, x).

theorem TauCeti.MooreLoopSpace.doubleHomologyAddEquiv_apply {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 2) X x)) (a : Additive (HomotopyGroup.Pi (n + 4) X x)) : (doubleHomologyAddEquiv x n hX) a = (homologyAddEquiv 1 n ⋯) (Additive.ofMul ((homotopyGroupMulEquiv x (n + 2)).symm (Additive.toMul a)))

TauCeti.MooreLoopSpace.doubleHomologyAddEquiv is the inverse Moore loop-space shift followed by the Hurewicz identification for the Moore loop space.

noncomputable def TauCeti.MooreLoopSpace.doubleCubicalHomologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 2) X x)) : Additive (HomotopyGroup.Pi (n + 4) X x) ≃+ ↑(HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) (n + 2))

With normalized cubical chains: if π_{k+2}(X, x) vanishes for every k < n + 2, then H_{n+2}(ΩᴹΩᴹX; ℤ) ≅ π_{n+4}(X, x), through TauCeti.singularCubicalHomologyIso.

theorem TauCeti.MooreLoopSpace.doubleCubicalHomologyAddEquiv_apply {X : Type} [TopologicalSpace X] (x : X) (n : ℕ) (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup.Pi (k + 2) X x)) (a : Additive (HomotopyGroup.Pi (n + 4) X x)) : (doubleCubicalHomologyAddEquiv x n hX) a = (ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularToCubical ℤ).app ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) (n + 2))) ((doubleHomologyAddEquiv x n hX) a)

The cubical identification is the singular one followed by the homology map of the named singular-to-cubical comparison.