Asphericity and covering spaces

A covering map p : E → X is an isomorphism on homotopy groups in every dimension at least two, so the higher homotopy of a cover and of its base are the same. Asphericity is therefore inherited in both directions along a covering map, the only extra input being path-connectedness of whichever space is not already known to be path-connected.

This file records that transfer and the two K(G, 1) recognition principles it yields.

• Downwards: the base of a surjective covering map with aspherical total space is aspherical. Combined with the identification of the fundamental group of the base of a simply connected quotient covering map, a group acting freely and properly discontinuously on a simply connected space whose higher homotopy vanishes has an orbit space of type K(G, 1). This is the standard way K(G, 1) spaces are produced.
• Upwards: a path-connected covering space of an aspherical space is aspherical. Its fundamental group is the subgroup of π₁ of the base recovered by p, because a covering map is injective on fundamental groups, so a path-connected cover of a K(G, 1) is a K(H, 1) for that subgroup H.

Taking the total space simply connected in the upwards direction says that the universal cover of an aspherical space is weakly contractible: all of its homotopy groups vanish, including π₁, which is where simple connectedness enters. Nothing here asserts that such a cover is contractible; that is a genuinely stronger statement, requiring a Whitehead-type theorem which this development does not have.

The ᵐᵒᵖ in Mathlib's IsQuotientCoveringMap.fundamentalGroupEquiv is invisible in the K(G, 1) statement below: being a K(G, 1) is invariant under MulEquiv.inv', the isomorphism G ≃* Gᵐᵒᵖ sending g to op g⁻¹.

This advances TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13, "K(G, 1) spaces", by supplying the covering-space recognition principle for them; the concrete circle and torus examples were proved directly.

Main declarations

• IsCoveringMap.subsingleton_homotopyGroup_iff: a cover and its base have the same higher homotopy groups.
• IsCoveringMap.isAspherical: the base of a surjective covering map with aspherical total space is aspherical.
• IsCoveringMap.isAspherical_totalSpace: a path-connected covering space of an aspherical space is aspherical.
• IsCoveringMap.subsingleton_homotopyGroup_of_isAspherical: the simply connected cover of an aspherical space is weakly contractible.
• IsCoveringMap.isEilenbergMacLaneSpaceOne_totalSpace: a path-connected cover of a K(G, 1) is a K(H, 1) for the subgroup H it recovers.
• IsQuotientCoveringMap.isEilenbergMacLaneSpaceOne: the orbit space of a free, properly discontinuous action of G on a simply connected space with vanishing higher homotopy is a K(G, 1).

References

The isomorphism on higher homotopy groups is TauCeti.IsCoveringMap.homotopyGroupPiMulEquiv; the injectivity of a covering map on fundamental groups is TauCeti.IsCoveringMap.mapOfEq_injective. The identification of the fundamental group of the base of a simply connected quotient covering map with the opposite of the acting group is Junyan Xu's IsQuotientCoveringMap.fundamentalGroupEquiv in Mathlib/Topology/Homotopy/Lifting.lean. Compare Proposition 4.1 and Section 1.B of [hatcher02]; no external formalization is copied or adapted here.

theorem IsCoveringMap.subsingleton_homotopyGroup_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {e : E} {x : X} (hp : IsCoveringMap p) (he : p e = x) (n : ℕ) : Subsingleton (HomotopyGroup.Pi (n + 2) E e) ↔ Subsingleton (HomotopyGroup.Pi (n + 2) X x)

A covering map identifies the homotopy groups of its total space in dimensions at least two with those of its base, so one is trivial exactly when the other is.

theorem IsCoveringMap.isAspherical {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {e : E} {x : X} (hp : IsCoveringMap p) (hp' : Function.Surjective p) (he : p e = x) (h : TauCeti.IsAspherical E e) : TauCeti.IsAspherical X x

The base of a surjective covering map with aspherical total space is aspherical.

theorem IsCoveringMap.isAspherical_totalSpace {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {e : E} {x : X} (hp : IsCoveringMap p) [PathConnectedSpace E] (he : p e = x) (h : TauCeti.IsAspherical X x) : TauCeti.IsAspherical E e

A path-connected covering space of an aspherical space is aspherical.

theorem IsCoveringMap.subsingleton_homotopyGroup_of_isAspherical {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {e : E} {x : X} (hp : IsCoveringMap p) [SimplyConnectedSpace E] (he : p e = x) (h : TauCeti.IsAspherical X x) (n : ℕ) : Subsingleton (HomotopyGroup.Pi (n + 1) E e)

The simply connected cover of an aspherical space is weakly contractible: every one of its homotopy groups in a positive dimension is trivial.

In dimension one this is simple connectedness of the cover; in the higher dimensions it is the asphericity of the base transported along the covering map.

theorem IsCoveringMap.isAspherical_of_subsingleton_homotopyGroup {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {e : E} {x : X} (hp : IsCoveringMap p) (hp' : Function.Surjective p) [PathConnectedSpace E] (he : p e = x) (h : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) E e)) : TauCeti.IsAspherical X x

A base covered by a path-connected space whose higher homotopy groups all vanish is aspherical. This is the recognition principle behind K(G, 1) spaces: the hypothesis is on the cover, and no homotopy group of the base has to be computed directly.

theorem IsCoveringMap.isEilenbergMacLaneSpaceOne_totalSpace {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {e : E} {x : X} (hp : IsCoveringMap p) [PathConnectedSpace E] (he : p e = x) (h : TauCeti.IsAspherical X x) : TauCeti.IsEilenbergMacLaneSpaceOne (↥(FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range) E e

A path-connected covering space of a K(G, 1) is a K(H, 1), for H the subgroup of the fundamental group of the base that the cover recovers.

The fundamental-group witness is MonoidHom.ofInjective applied to the injectivity of p on fundamental groups; the recovered subgroup is by definition the range of that map.

theorem IsQuotientCoveringMap.isEilenbergMacLaneSpaceOne {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {e : E} {x : X} {G : Type u_3} [Group G] [MulAction G E] {f : E → X} (hf : IsQuotientCoveringMap f G) [SimplyConnectedSpace E] (he : f e = x) (h : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) E e)) : TauCeti.IsEilenbergMacLaneSpaceOne G X x

The orbit space of a free, properly discontinuous action of G on a simply connected space all of whose higher homotopy groups vanish is a K(G, 1).

The hypotheses are packaged as a quotient covering map, which is exactly freeness together with the local disjointness making the orbit map a covering. The fundamental group of the orbit space is the opposite group Gᵐᵒᵖ, which is isomorphic to G by MulEquiv.inv'.