Aspherical spaces through the universal cover and its subgroup quotients

Under the standing hypotheses of this development — X path-connected, locally path-connected and semilocally simply connected — every homotopy group of X in a dimension at least two is a homotopy group of the universal cover. Asphericity of X is therefore a property of the universal cover alone: X is aspherical exactly when the higher homotopy groups of UniversalCover x₀ vanish. Since the universal cover is simply connected, that condition says precisely that it is weakly contractible.

This turns the Galois correspondence of Stage 2 into a statement about Eilenberg--Mac Lane spaces. Every subgroup H ≤ π₁(X, x₀) is realised by the connected cover UniversalCover x₀ / H, whose fundamental group is Hᵐᵒᵖ, hence isomorphic to H; when X is a K(G, 1) that cover is aspherical too, so it is a K(H, 1). In particular every subgroup of the fundamental group of a K(G, 1) is isomorphic to the fundamental group of a K(H, 1) realised as a covering space of X.

The general covering-space input is IsCoveringMap.isAspherical_totalSpace; the only work here is to supply the universal cover and the covers attached to subgroups as instances of it, with their distinguished basepoints.

This advances TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13, "K(G, 1) spaces", by tying that item to the Stage 2 classification: the covers produced by item 7 of that stage are Eilenberg--Mac Lane spaces whenever the base is.

Main declarations

• TauCeti.UniversalCover.isAspherical_iff: a space is aspherical exactly when the higher homotopy groups of its universal cover vanish.
• TauCeti.UniversalCover.isEilenbergMacLaneSpaceOne: the resulting K(G, 1) recognition principle.
• TauCeti.UniversalCover.isAspherical_subgroupQuotient and TauCeti.UniversalCover.isEilenbergMacLaneSpaceOne_subgroupQuotient: the cover attached to H ≤ π₁(X, x₀) over a K(G, 1) is a K(H, 1).

References

The cover attached to a subgroup and its fundamental group come from TauCeti.AlgebraicTopology.UniversalCover.Classification.Existence and …Classification.RecoveredSubgroup, which adapt Kim Morrison's universal-cover construction in mathlib4#38292 and use Junyan Xu's quotient-covering API in Mathlib/Topology/Homotopy/Lifting.lean. Compare Section 1.B of [hatcher02]; no external formalization is copied or adapted here.

theorem TauCeti.UniversalCover.isAspherical_iff {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : IsAspherical X x₀ ↔ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) (UniversalCover x₀) ↑(basepointLift x₀))

A space is aspherical exactly when the higher homotopy groups of its universal cover vanish.

Together with simple connectedness of the universal cover, the right-hand side says that the universal cover is weakly contractible.

theorem TauCeti.UniversalCover.isEilenbergMacLaneSpaceOne {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) {G : Type u_2} [Group G] (e : FundamentalGroup X x₀ ≃* G) (h : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) (UniversalCover x₀) ↑(basepointLift x₀))) : IsEilenbergMacLaneSpaceOne G X x₀

A space whose universal cover has vanishing higher homotopy groups is a K(G, 1), for any group G isomorphic to its fundamental group.

theorem TauCeti.UniversalCover.isAspherical_subgroupQuotient {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) (h : IsAspherical X x₀) : IsAspherical (SubgroupQuotient x₀ H) (SubgroupQuotient.basepoint x₀ H)

The cover of an aspherical space attached to a subgroup of its fundamental group is aspherical.

theorem TauCeti.UniversalCover.isEilenbergMacLaneSpaceOne_subgroupQuotient {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) (h : IsAspherical X x₀) : IsEilenbergMacLaneSpaceOne (↥H) (SubgroupQuotient x₀ H) (SubgroupQuotient.basepoint x₀ H)

The cover attached to H ≤ π₁(X, x₀) over a K(G, 1) is a K(H, 1).

So every subgroup of the fundamental group of an aspherical space is isomorphic to the fundamental group of an aspherical covering space of it. The ᵐᵒᵖ recorded by TauCeti.UniversalCover.SubgroupQuotient.fundamentalGroupEquiv disappears along MulEquiv.inv'.