First homology of loop spaces

For a path-connected based loop space, degree-one Hurewicz and the loop-space shift identify its integral first homology with the second homotopy group of the original space. The abelianization disappears because higher homotopy groups are commutative.

When π₂(X, x) vanishes, the double Moore loop space is path connected and H₁(ΩᴹΩᴹX; ℤ) ≅ π₃(X, x). This is the low-degree homological input to detecting higher homotopy through double loop spaces. The Moore comparisons use the specified normalization homotopy equivalences; the final doubleFirstCubicalHomologyAddEquiv transports the result to normalized cubical homology through singularCubicalHomologyIso. No connectedness assumption on X is needed.

References

• A. Hatcher, Algebraic Topology, Theorem 2A.1 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, Proposition 5.11.

noncomputable def TauCeti.pathLoopSpaceFirstHomologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace (LoopSpace X x)] : Additive (HomotopyGroup.Pi 2 X x) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(LoopSpace X x)) 1)

Degree-one Hurewicz identifies the first integral homology of a path-connected loop space with the second homotopy group of the original space.

@[simp]

theorem TauCeti.pathLoopSpaceFirstHomologyAddEquiv_symm_loopClass {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace (LoopSpace X x)] (γ : Path (Path.refl x) (Path.refl x)) : (pathLoopSpaceFirstHomologyAddEquiv x).symm ((HurewiczOne.H₁AddEquivHomology ↧(LoopSpace X x)) (HurewiczOne.loopClass γ)) = Additive.ofMul ((HomotopyGroup.pathLoopSpaceMulEquiv 0) (HomotopyGroup.pi1MulEquivFundamentalGroup.symm (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ))))

The inverse Hurewicz isomorphism sends the homology class of a loop of loops to its class under the loop-space shift.

noncomputable def TauCeti.MooreLoopSpace.firstHomologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace (MooreLoopSpace X x)] : Additive (HomotopyGroup.Pi 2 X x) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace X x)) 1)

Normalization identifies the first integral homology of a path-connected Moore loop space with the second homotopy group of the original space.

noncomputable def TauCeti.MooreLoopSpace.doubleFirstHomologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) [Subsingleton (HomotopyGroup.Pi 2 X x)] : Additive (HomotopyGroup.Pi 3 X x) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) 1)

When π₂(X, x) vanishes, the first integral homology of the double Moore loop space is the third homotopy group of X, using the specified normalization comparisons.

theorem TauCeti.MooreLoopSpace.firstHomologyAddEquiv_symm_apply {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace (MooreLoopSpace X x)] (a : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace X x)) 1)) : (firstHomologyAddEquiv x).symm a = (pathLoopSpaceFirstHomologyAddEquiv x).symm ((ModuleCat.Hom.hom ((homotopyEquivPath x).singularHomologyIso (↧ℤ) 1).hom) a)

The inverse comparison computes a Moore-loop homology class by normalizing it to fixed-interval loops and applying the inverse Hurewicz isomorphism.

theorem TauCeti.MooreLoopSpace.doubleFirstHomologyAddEquiv_symm_apply {X : Type} [TopologicalSpace X] (x : X) [Subsingleton (HomotopyGroup.Pi 2 X x)] (a : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) 1)) : (doubleFirstHomologyAddEquiv x).symm a = (MulEquiv.toAdditive (homotopyGroupMulEquiv x 1)) ((firstHomologyAddEquiv 1).symm a)

The inverse double-loop comparison applies the inverse first-homology comparison and then the Moore loop-space shift.

noncomputable def TauCeti.MooreLoopSpace.doubleFirstCubicalHomologyAddEquiv {X : Type} [TopologicalSpace X] (x : X) [Subsingleton (HomotopyGroup.Pi 2 X x)] : Additive (HomotopyGroup.Pi 3 X x) ≃+ ↑(HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) 1)

With normalized cubical chains, the first homology of the double Moore loop space is the third homotopy group of the original space when its second homotopy group vanishes.

theorem TauCeti.MooreLoopSpace.doubleFirstCubicalHomologyAddEquiv_apply {X : Type} [TopologicalSpace X] (x : X) [Subsingleton (HomotopyGroup.Pi 2 X x)] (a : Additive (HomotopyGroup.Pi 3 X x)) : (doubleFirstCubicalHomologyAddEquiv x) a = (ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularToCubical ℤ).app ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) 1)) ((doubleFirstHomologyAddEquiv x) a)

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