A covering map induces isomorphisms on higher homotopy groups

Let p : E → X be a covering map and let e : E. This file shows that postcomposition with p identifies the homotopy groups of E at e with those of X at p e, in every dimension ≥ 2.

Both halves are consequences of Mathlib's covering-space lifting toolkit.

• Injectivity holds already in dimension ≥ 1. Two generalized loops in E whose postcompositions with p are homotopic relative to the cube boundary are themselves homotopic relative to the cube boundary: this is Mathlib's IsCoveringMap.homotopicRel_iff_comp, whose hypothesis "the two maps agree at a point of the relative set" is supplied by the corner 0 of the cube, where both generalized loops take the value e.
• Surjectivity needs dimension ≥ 2. Splitting off one cube coordinate turns a generalized loop f : I^N → X into a homotopy I × I^{j ≠ i} → X starting at the constant map p e. Mathlib's IsCoveringMap.liftHomotopyRel lifts it relative to the boundary of the remaining coordinates, so the lift is constant there and at both ends of the split coordinate. A second coordinate, supplied by Nontrivial N, ensures that every boundary face is of one of these forms.

The conclusion is packaged as a multiplicative equivalence π_n(E, e) ≃* π_n(X, p e) for n ≥ 2, in the general indexed form and in the Fin (n + 2) form.

This is Stage 3, item 10 of the Tau Ceti universal-covers roadmap (TauCetiRoadmap/UniversalCovers/README.md): "p_* : π_n(X̃) ≅ π_n(X) for n ≥ 2, any cover".

Main declarations

• GenLoop.map_homotopic_iff: postcomposition with a covering map reflects (and preserves) homotopy of generalized loops.
• GenLoop.map_surjective: in dimension ≥ 2, every generalized loop in the base lifts to a generalized loop in the total space based at a prescribed point of the fibre.
• HomotopyGroup.map_injective, HomotopyGroup.map_surjective: the induced map on homotopy classes.
• IsCoveringMap.homotopyGroupMulEquiv: the isomorphism HomotopyGroup N E e ≃* HomotopyGroup N X (p e) for [Nontrivial N].
• IsCoveringMap.homotopyGroupPiMulEquiv: its π_(n + 2) form.

References

The lifting machinery consumed here (IsCoveringMap.liftHomotopyRel, IsCoveringMap.homotopicRel_iff_comp) is Junyan Xu's covering-space API in Mathlib.Topology.Homotopy.Lifting and Mathlib.Topology.Covering.Basic. Compare Proposition 4.1 of [hatcher02].

@[simp]

theorem GenLoop.map_homotopic_iff {N : Type u_1} {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {p : E → X} {e : E} [Nonempty N] (hp : IsCoveringMap p) {F G : ↑(GenLoop N E e)} : Homotopic (map { toFun := p, continuous_toFun := ⋯ } ⋯ F) (map { toFun := p, continuous_toFun := ⋯ } ⋯ G) ↔ Homotopic F G

Postcomposition with a covering map p neither creates nor destroys homotopies between generalized loops in the total space: two generalized loops based at e are homotopic relative to the cube boundary if and only if their postcompositions with p are.

The reverse implication is GenLoop.map_homotopic and needs no hypothesis on p; the forward implication lifts the homotopy, using that both generalized loops take the value e at the corner 0 of the cube.

theorem GenLoop.map_surjective {N : Type u_1} {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {p : E → X} {e : E} [Nontrivial N] (hp : IsCoveringMap p) (f : ↑(GenLoop N X (p e))) : ∃ (F : ↑(GenLoop N E e)), map { toFun := p, continuous_toFun := ⋯ } ⋯ F = f

Every generalized loop in the base of a covering map lifts, in dimensions ≥ 2, to a generalized loop in the total space based at any prescribed point e of the fibre.

The index type is assumed nontrivial (equivalently: the dimension is at least 2), so after splitting off one coordinate there is another coordinate whose boundary can be held fixed by a relative homotopy lift. In dimension 1 the statement is false: a loop in the base lifts to a path in the total space, whose endpoint need not return to e.

theorem HomotopyGroup.map_injective {N : Type u_1} {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {p : E → X} {e : E} [Nonempty N] (hp : IsCoveringMap p) : Function.Injective (map { toFun := p, continuous_toFun := ⋯ } ⋯)

A covering map is injective on homotopy groups in every positive dimension.

theorem HomotopyGroup.map_surjective {N : Type u_1} {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {p : E → X} {e : E} [Nontrivial N] (hp : IsCoveringMap p) : Function.Surjective (map { toFun := p, continuous_toFun := ⋯ } ⋯)

A covering map is surjective on homotopy groups in dimensions ≥ 2.

noncomputable def IsCoveringMap.homotopyGroupMulEquiv {N : Type u_1} {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {p : E → X} [DecidableEq N] [Nontrivial N] (hp : IsCoveringMap p) (e : E) : HomotopyGroup N E e ≃* HomotopyGroup N X (p e)

A covering map induces an isomorphism on homotopy groups in dimensions ≥ 2.

Postcomposition with p is a group isomorphism π_N(E, e) ≃* π_N(X, p e) whenever the index type N has at least two elements. No connectivity hypothesis on E or X is needed: both halves are statements about lifting cubes.

Equations

• hp.homotopyGroupMulEquiv e = MulEquiv.ofBijective (HomotopyGroup.mapHom { toFun := p, continuous_toFun := ⋯ } ⋯) ⋯

@[simp]

theorem IsCoveringMap.homotopyGroupMulEquiv_apply {N : Type u_1} {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {p : E → X} [DecidableEq N] [Nontrivial N] (hp : IsCoveringMap p) (e : E) (a : HomotopyGroup N E e) : (hp.homotopyGroupMulEquiv e) a = HomotopyGroup.map { toFun := p, continuous_toFun := ⋯ } ⋯ a

noncomputable def IsCoveringMap.homotopyGroupPiMulEquiv {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {p : E → X} (hp : IsCoveringMap p) (e : E) (n : ℕ) : HomotopyGroup.Pi (n + 2) E e ≃* HomotopyGroup.Pi (n + 2) X (p e)

The π_(n + 2) form of IsCoveringMap.homotopyGroupMulEquiv: a covering map p : E → X induces π_(n + 2)(E, e) ≃* π_(n + 2)(X, p e) for every n : ℕ.

Equations

• hp.homotopyGroupPiMulEquiv e n = hp.homotopyGroupMulEquiv e

@[simp]

theorem IsCoveringMap.homotopyGroupPiMulEquiv_apply {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {p : E → X} (hp : IsCoveringMap p) (e : E) (n : ℕ) (a : HomotopyGroup.Pi (n + 2) E e) : (hp.homotopyGroupPiMulEquiv e n) a = HomotopyGroup.map { toFun := p, continuous_toFun := ⋯ } ⋯ a