Acyclicity of loop spaces and aspherical spaces

For a pointed space (X, x), the loop-space shift identifies πₖ(ΩX) with πₖ₊₁(X, x) in every degree k ≥ 0, and therefore identifies πₖ(Ω²X) with πₖ₊₂(X, x). Combined with Eilenberg's based-cube retraction (TauCeti.isZero_homology_normalizedCubicalChainComplex_of_subsingleton_homotopyGroup) and the higher cubical Hurewicz isomorphism (HomotopyGroup.cubicalHurewiczAddEquiv and HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv), this yields the homological characterization of vanishing higher homotopy groups:

• A loop space ΩX (or ΩᴹX) is path connected with vanishing positive-degree integral homology if and only if πₙ₊₁(X, x) is trivial for every n : ℕ.
• A double loop space Ω²X (or ΩᴹΩᴹX) is path connected with vanishing positive-degree integral homology if and only if πₙ₊₂(X, x) is trivial for every n : ℕ.
• In particular, when X is path connected, Ω²X (or ΩᴹΩᴹX) has the integral homology of a point if and only if X is aspherical (TauCeti.IsAspherical), i.e., an Eilenberg--Mac Lane space K(π₁(X, x), 1) (TauCeti.IsEilenbergMacLaneSpaceOne). In the forward direction, the positive-degree homology of Ω²X and ΩᴹΩᴹX vanishes with coefficients in any ring.
• If πₙ₊₂(X, x) is trivial for every n : ℕ, the Moore loop space ΩᴹX itself has no homology in positive degrees, with coefficients in any ring, although it need not be path connected: its path components are the elements of π₁(X, x), and each of them is weakly contractible.

Both the fixed-interval and Moore loop-space models, as well as simplicial singular chains and normalized cubical chains, are treated.

The arbitrary-ring vanishing results allow X : Type u and R : Type u. The integral-homology characterizations use X : Type: the chain functors singularChains and normalizedCubicalChainComplex share the universe of the space and coefficient ring, so their specializations to ℤ take small spaces. The Hurewicz equivalences used here have the same scope.

Main results

• TauCeti.isZero_homology_normalizedCubicalChainComplex_doubleLoopSpace, TauCeti.isZero_homology_singularChains_doubleLoopSpace, TauCeti.MooreLoopSpace.isZero_homology_normalizedCubicalChainComplex_double, TauCeti.MooreLoopSpace.isZero_homology_singularChains_double: vanishing of the positive-degree homology of Ω²X and ΩᴹΩᴹX over any coefficient ring when πₙ₊₂(X, x) vanishes for all n.
• TauCeti.MooreLoopSpace.isZero_homology_normalizedCubicalChainComplex_of_forall_subsingleton, TauCeti.MooreLoopSpace.isZero_homology_singularChains_of_forall_subsingleton: under the same hypothesis, vanishing of the positive-degree homology of ΩᴹX.
• TauCeti.pathConnectedSpace_doubleLoopSpace_and_forall_isZero_homology_singularChains_iff, TauCeti.MooreLoopSpace.pathConnectedSpace_double_and_forall_isZero_homology_singularChains_iff: Ω²X and ΩᴹΩᴹX have the integral homology of a point if and only if πₙ₊₂(X, x) vanishes for all n.
• TauCeti.isAspherical_iff_doubleLoopSpace_singularHomology, TauCeti.isAspherical_iff_doubleLoopSpace_cubicalHomology, TauCeti.MooreLoopSpace.isAspherical_iff_double_singularHomology, TauCeti.MooreLoopSpace.isAspherical_iff_double_cubicalHomology: for path-connected X, Ω²X and ΩᴹΩᴹX have the integral homology of a point if and only if X is aspherical / a K(π₁(X, x), 1) (Barraud--Damian--Humilière--Oancea, Lemma 3.41).

References

• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, Lemma 3.41.
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, §4.1 and Theorem 4.32.

Vanishing of positive-degree homology over an arbitrary coefficient ring

theorem TauCeti.isZero_homology_normalizedCubicalChainComplex_loopSpace {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex R).obj ↧(LoopSpace X x)) m)

If π_ (n + 1) X x vanishes for all n : ℕ, then the positive-degree normalized cubical homology of Ω X x vanishes over any coefficient ring R.

theorem TauCeti.isZero_homology_singularChains_loopSpace {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains R).obj ↧(LoopSpace X x)) m)

If π_ (n + 1) X x vanishes for all n : ℕ, then the positive-degree singular homology of Ω X x vanishes over any coefficient ring R.

theorem TauCeti.isZero_homology_normalizedCubicalChainComplex_doubleLoopSpace {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex R).obj ↧(LoopSpace (LoopSpace X x) (Path.refl x))) m)

If π_ (n + 2) X x vanishes for all n : ℕ, then the positive-degree normalized cubical homology of Ω (Ω X x) (Path.refl x) vanishes over any coefficient ring R.

theorem TauCeti.isZero_homology_singularChains_doubleLoopSpace {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains R).obj ↧(LoopSpace (LoopSpace X x) (Path.refl x))) m)

If π_ (n + 2) X x vanishes for all n : ℕ, then the positive-degree singular homology of Ω (Ω X x) (Path.refl x) vanishes over any coefficient ring R.

theorem TauCeti.MooreLoopSpace.isZero_homology_normalizedCubicalChainComplex {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex R).obj ↧(MooreLoopSpace X x)) m)

If π_ (n + 1) X x vanishes for all n : ℕ, then the positive-degree normalized cubical homology of MooreLoopSpace X x vanishes over any coefficient ring R.

theorem TauCeti.MooreLoopSpace.isZero_homology_singularChains {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains R).obj ↧(MooreLoopSpace X x)) m)

If π_ (n + 1) X x vanishes for all n : ℕ, then the positive-degree singular homology of MooreLoopSpace X x vanishes over any coefficient ring R.

theorem TauCeti.MooreLoopSpace.isZero_homology_normalizedCubicalChainComplex_double {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex R).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) m)

If π_ (n + 2) X x vanishes for all n : ℕ, then the positive-degree normalized cubical homology of the double Moore loop space vanishes over any coefficient ring R.

theorem TauCeti.MooreLoopSpace.isZero_homology_singularChains_double {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains R).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) m)

If π_ (n + 2) X x vanishes for all n : ℕ, then the positive-degree singular homology of the double Moore loop space vanishes over any coefficient ring R.

theorem TauCeti.MooreLoopSpace.isZero_homology_normalizedCubicalChainComplex_of_forall_subsingleton {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex R).obj ↧(MooreLoopSpace X x)) m)

The Moore loop space of an aspherical space has no homology in positive degrees. If π_ (n + 2) X x vanishes for all n : ℕ, then the positive-degree normalized cubical homology of MooreLoopSpace X x vanishes over any coefficient ring R. The loop space need not be path connected: its path components are the elements of π₁(X, x), and each of them is weakly contractible.

theorem TauCeti.MooreLoopSpace.isZero_homology_singularChains_of_forall_subsingleton {X : Type u} [TopologicalSpace X] (R : Type u) [Ring R] {x : X} (hX : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)) {m : ℕ} (hm0 : m ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains R).obj ↧(MooreLoopSpace X x)) m)

The Moore loop space of an aspherical space has no singular homology in positive degrees. If π_ (n + 2) X x vanishes for all n : ℕ, then the positive-degree singular homology of MooreLoopSpace X x vanishes over any coefficient ring R.

Homological characterization via the Hurewicz isomorphism

theorem TauCeti.pathConnectedSpace_loopSpace_and_forall_isZero_homology_singularChains_iff {X : Type} [TopologicalSpace X] (x : X) : (PathConnectedSpace (LoopSpace X x) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains ℤ).obj ↧(LoopSpace X x)) m)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)

The fixed-interval loop space Ω X x is path connected with vanishing positive-degree integral singular homology if and only if π_ (n + 1) X x is trivial for every n : ℕ.

theorem TauCeti.pathConnectedSpace_loopSpace_and_forall_isZero_homology_normalizedCubicalChainComplex_iff {X : Type} [TopologicalSpace X] (x : X) : (PathConnectedSpace (LoopSpace X x) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧(LoopSpace X x)) m)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)

The fixed-interval loop space Ω X x is path connected with vanishing positive-degree integral normalized cubical homology if and only if π_ (n + 1) X x is trivial for every n : ℕ.

theorem TauCeti.pathConnectedSpace_doubleLoopSpace_and_forall_isZero_homology_singularChains_iff {X : Type} [TopologicalSpace X] (x : X) : (PathConnectedSpace (LoopSpace (LoopSpace X x) (Path.refl x)) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains ℤ).obj ↧(LoopSpace (LoopSpace X x) (Path.refl x))) m)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)

The fixed-interval double loop space Ω (Ω X x) (Path.refl x) is path connected with vanishing positive-degree integral singular homology if and only if π_ (n + 2) X x is trivial for every n : ℕ.

theorem TauCeti.pathConnectedSpace_doubleLoopSpace_and_forall_isZero_homology_normalizedCubicalChainComplex_iff {X : Type} [TopologicalSpace X] (x : X) : (PathConnectedSpace (LoopSpace (LoopSpace X x) (Path.refl x)) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧(LoopSpace (LoopSpace X x) (Path.refl x))) m)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)

The fixed-interval double loop space Ω (Ω X x) (Path.refl x) is path connected with vanishing positive-degree integral normalized cubical homology if and only if π_ (n + 2) X x is trivial for every n : ℕ.

theorem TauCeti.isAspherical_iff_doubleLoopSpace_singularHomology {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace X] : IsAspherical X x ↔ PathConnectedSpace (LoopSpace (LoopSpace X x) (Path.refl x)) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains ℤ).obj ↧(LoopSpace (LoopSpace X x) (Path.refl x))) m)

Barraud--Damian--Humilière--Oancea, Lemma 3.41 (fixed-interval singular homology). A path-connected space X is aspherical if and only if its double loop space Ω (Ω X x) (Path.refl x) is path connected with vanishing positive-degree integral singular homology.

theorem TauCeti.isAspherical_iff_doubleLoopSpace_cubicalHomology {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace X] : IsAspherical X x ↔ PathConnectedSpace (LoopSpace (LoopSpace X x) (Path.refl x)) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧(LoopSpace (LoopSpace X x) (Path.refl x))) m)

Barraud--Damian--Humilière--Oancea, Lemma 3.41 (fixed-interval cubical homology). A path-connected space X is aspherical if and only if its double loop space Ω (Ω X x) (Path.refl x) is path connected with vanishing positive-degree integral normalized cubical homology.

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_and_forall_isZero_homology_singularChains_iff {X : Type} [TopologicalSpace X] (x : X) : (PathConnectedSpace (MooreLoopSpace X x) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace X x)) m)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)

The Moore loop space MooreLoopSpace X x is path connected with vanishing positive-degree integral singular homology if and only if π_ (n + 1) X x is trivial for every n : ℕ.

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_and_forall_isZero_homology_normalizedCubicalChainComplex_iff {X : Type} [TopologicalSpace X] (x : X) : (PathConnectedSpace (MooreLoopSpace X x) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧(MooreLoopSpace X x)) m)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)

The Moore loop space MooreLoopSpace X x is path connected with vanishing positive-degree integral normalized cubical homology if and only if π_ (n + 1) X x is trivial for every n : ℕ.

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_double_and_forall_isZero_homology_singularChains_iff {X : Type} [TopologicalSpace X] (x : X) : (PathConnectedSpace (MooreLoopSpace (MooreLoopSpace X x) 1) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) m)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)

The double Moore loop space MooreLoopSpace (MooreLoopSpace X x) 1 is path connected with vanishing positive-degree integral singular homology if and only if π_ (n + 2) X x is trivial for every n : ℕ.

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_double_and_forall_isZero_homology_normalizedCubicalChainComplex_iff {X : Type} [TopologicalSpace X] (x : X) : (PathConnectedSpace (MooreLoopSpace (MooreLoopSpace X x) 1) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) m)) ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)

The double Moore loop space MooreLoopSpace (MooreLoopSpace X x) 1 is path connected with vanishing positive-degree integral normalized cubical homology if and only if π_ (n + 2) X x is trivial for every n : ℕ.

theorem TauCeti.MooreLoopSpace.isAspherical_iff_double_singularHomology {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace X] : IsAspherical X x ↔ PathConnectedSpace (MooreLoopSpace (MooreLoopSpace X x) 1) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((singularChains ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) m)

Barraud--Damian--Humilière--Oancea, Lemma 3.41 (Moore singular homology). A path-connected space X is aspherical if and only if its double Moore loop space is path connected with vanishing positive-degree integral singular homology.

theorem TauCeti.MooreLoopSpace.isAspherical_iff_double_cubicalHomology {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace X] : IsAspherical X x ↔ PathConnectedSpace (MooreLoopSpace (MooreLoopSpace X x) 1) ∧ ∀ (m : ℕ), m ≠ 0 → CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧(MooreLoopSpace (MooreLoopSpace X x) 1)) m)

Barraud--Damian--Humilière--Oancea, Lemma 3.41 (Moore cubical homology). A path-connected space X is aspherical if and only if its double Moore loop space is path connected with vanishing positive-degree integral normalized cubical homology.