Covering maps, lifting criteria, and fundamental-group monodromy

This file records generic covering-space consequences of Mathlib's path-lifting and monodromy API. For a covering map p : E → X whose total space is simply connected, choosing a lift e over x identifies π₁(X, x) with the fibre over x by sending a loop class to its monodromy translate of e.

It also records that a covering map is injective on fundamental groups — the fundamental-group form of Mathlib's IsCoveringMap.injective_path_homotopic_map, which states the same injectivity for the Hom-sets of the fundamental groupoid. Dually, a covering map of a path-connected space onto a simply connected space is injective: a path joining two points of a fibre projects to a loop, which is null-homotopic, so its lift is a loop as well.

It also records the lifting criterion in a subgroup form used by the universal-covers roadmap. Mathlib already proves the fundamental result IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le: a map f : A → X lifts through a covering map p : E → X, with prescribed basepoint lift e₀, when f_* π₁(A, a₀) is contained in p_* π₁(E, e₀). The classification of covers often inserts an intermediate subgroup H ≤ π₁(X, f a₀): one first proves f_* π₁(A, a₀) ≤ H, and separately identifies H as a subgroup of the image of p_*.

Main declarations

• IsCoveringMap.map_injective and IsCoveringMap.mapOfEq_injective: a covering map is injective on fundamental groups.
• IsCoveringMap.injective: a covering map from a path-connected space to a simply connected space is injective.
• IsCoveringMapOn.injective_of_range_subset: the same for a covering map over a set, when its range lies in a simply connected subset of that set.
• IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le_subgroup: lift when f_* π₁(A, a₀) ≤ H ≤ p_* π₁(E, e₀).
• IsCoveringMap.existsUnique_continuousMap_lifts_of_subsingleton_fundamentalGroup: lift when the source fundamental group is subsingleton.
• IsCoveringMap.fundamentalGroupEquivFiber: the monodromy bijection FundamentalGroup X x ≃ p ⁻¹' {x}, γ ↦ monodromy γ e.
• IsCoveringMap.fundamentalGroupEquivFiber_apply_symm_apply: the inverse sends a fibre point to the loop class whose monodromy translate of the chosen lift is that point.

References

This builds directly on Junyan Xu's covering-space lifting and monodromy API in Mathlib.Topology.Homotopy.Lifting. The subgroup lifting criterion is a thin wrapper around Mathlib's IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le, and uses the trivial-source fundamental-group range lemmas from TauCeti.AlgebraicTopology.FundamentalGroup.Basic.

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

A covering map induces an injective map on fundamental groups. This is the fundamental-group form of Mathlib's IsCoveringMap.injective_path_homotopic_map, which states the same injectivity for every Hom-set of the fundamental groupoid.

theorem IsCoveringMap.mapOfEq_injective {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} (hp : IsCoveringMap p) {e : E} (he : p e = x) : Function.Injective ⇑(FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } he)

A covering map induces an injective map on fundamental groups, in the form transported along an equality p e = x of basepoints.

Combined with MonoidHom.ofInjective, this exhibits the image subgroup p_* π₁(E, e) as a copy of π₁(E, e).

theorem IsCoveringMap.injective {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} [PathConnectedSpace E] [SimplyConnectedSpace X] (hp : IsCoveringMap p) : Function.Injective p

A covering map from a path-connected space to a simply connected space is injective.

theorem IsCoveringMapOn.injective_of_range_subset {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} [PathConnectedSpace E] {s t : Set X} (hp : IsCoveringMapOn p s) (hts : t ⊆ s) [SimplyConnectedSpace ↑t] (hpt : Set.range p ⊆ t) : Function.Injective p

A covering map whose range lies in a simply connected part of its base is injective. If p : E → X is a covering map over s, its total space is path-connected, and its range lies in a simply connected subset t ⊆ s, then p is injective.

theorem IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le_subgroup {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {A : Type u_3} [TopologicalSpace A] (hp : IsCoveringMap p) [PathConnectedSpace A] [LocallyPathConnectedSpace A] {f : C(A, X)} {a₀ : A} {e₀ : E} (he : p e₀ = f a₀) (H : Subgroup (FundamentalGroup X (f a₀))) (hfH : (FundamentalGroup.map f a₀).range ≤ H) (hHp : H ≤ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range) : ∃! F : C(A, E), F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

The lifting criterion for a covering map, with the subgroup inclusion factored through an intermediate subgroup H ≤ π₁(X, f a₀).

This is the form used when a cover is known to have recovered subgroup H: to lift f, it suffices to show that f_* π₁(A, a₀) lies in H, and that H is contained in the image of p_* π₁(E, e₀).

theorem IsCoveringMap.existsUnique_continuousMap_lifts_of_subsingleton_fundamentalGroup {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {A : Type u_3} [TopologicalSpace A] (hp : IsCoveringMap p) [PathConnectedSpace A] [LocallyPathConnectedSpace A] {f : C(A, X)} {a₀ : A} {e₀ : E} [Subsingleton (FundamentalGroup A a₀)] (he : p e₀ = f a₀) : ∃! F : C(A, E), F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

The lifting criterion when the source fundamental group at a₀ is subsingleton. In this case the induced subgroup f_* π₁(A, a₀) is trivial.

noncomputable def IsCoveringMap.fundamentalGroupEquivFiber {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : FundamentalGroup X x ≃ ↑(p ⁻¹' {x})

Choosing a basepoint lift e in the fibre over x identifies the fundamental group of the base with that fibre, via γ ↦ monodromy γ e.

Equations

• One or more equations did not get rendered due to their size.

theorem IsCoveringMap.fundamentalGroupEquivFiber_apply_coe {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (γ : FundamentalGroup X x) : ↑((hp.fundamentalGroupEquivFiber e) γ) = ↑(hp.monodromy γ e)

The general fibre equivalence sends a loop class to the monodromy translate of the chosen lift, as an equality in the total space E.

@[simp]

theorem IsCoveringMap.fundamentalGroupEquivFiber_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (γ : FundamentalGroup X x) : (hp.fundamentalGroupEquivFiber e) γ = hp.monodromy γ e

The general fibre equivalence sends a loop class to the monodromy translate of the chosen lift, as an equality in the fibre subtype.

@[simp]

theorem IsCoveringMap.fundamentalGroupEquivFiber_apply_symm_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hp : IsCoveringMap p) (e e' : ↑(p ⁻¹' {x})) : hp.monodromy ((hp.fundamentalGroupEquivFiber e).symm e') e = e'

The inverse of the general fibre equivalence is characterized by the loop class whose monodromy sends the chosen lift to the requested fibre point.

theorem IsCoveringMap.fundamentalGroupEquivFiber_apply_symm_apply_coe {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [SimplyConnectedSpace E] (hp : IsCoveringMap p) (e e' : ↑(p ⁻¹' {x})) : ↑(hp.monodromy ((hp.fundamentalGroupEquivFiber e).symm e') e) = ↑e'

On underlying points, the inverse of the general fibre equivalence is characterized by the loop class whose monodromy sends the chosen lift to the requested fibre point.