The subgroup a cover recovers from a chosen lift of the basepoint

Let p : E → X be a covering map and let e be a point of the fibre over x. Mathlib's IsCoveringMap.fundamentalGroupMulAction makes π₁(X, x) act on that fibre by monodromy. This file identifies the stabiliser of e for that action with the image of π₁(E, e) under p:

MulAction.stabilizer (π₁(X, x)) e = (FundamentalGroup.mapOfEq ⟨p, hp.continuous⟩ e.2).range.

That image is the subgroup the classification of covering spaces attaches to the pointed cover (E, e), so the identification is the bridge between the topological side (which loops of the base lift to loops of the cover) and the group-theoretic side (which subgroup of π₁(X, x) is recovered).

Three consequences follow, and are the reason the identification is worth isolating.

• A covering map is injective on fundamental groups (IsCoveringMap.mapOfEq_injective, in TauCeti.Topology.Homotopy.Covering), so the recovered subgroup is a copy of π₁(E, e) itself.
• When E is path connected the monodromy action is transitive, so the orbit-stabiliser theorem turns the fibre into the coset space of the recovered subgroup; in particular the number of sheets of the cover is the index of that subgroup.
• Changing the lift e inside the fibre conjugates the recovered subgroup, and when E is path connected every conjugate arises this way: a pointed cover recovers a subgroup, an unpointed connected cover only its conjugacy class. The recovered subgroup is normal exactly when it does not depend on the chosen lift.

Mathlib proves the analogous statement IsQuotientCoveringMap.ker_monodromyPerm only for a cover presented as a quotient by a group action, where the stabiliser of a single point is automatically the kernel of the whole monodromy representation. For a general cover the two subgroups differ, and it is the stabiliser, not the kernel, that the classification uses.

Main declarations

• IsCoveringMap.coe_monodromy_mk: monodromy along a path is the endpoint of its lift.
• TauCeti.coveringFiberEquiv: monodromy along a homotopy class of paths is a bijection between the fibres over its endpoints.
• IsCoveringMap.toPermHom_eq_monodromyPerm: the permutation representation of the monodromy action is IsCoveringMap.monodromyPerm.
• IsCoveringMap.monodromy_eq_self_iff_mem_range: a loop class of the base fixes the chosen lift under monodromy exactly when it is the image of a loop class of the cover.
• IsCoveringMap.stabilizer_eq_range, IsCoveringMap.comap_stabilizer_monodromyPerm: the same statement for the monodromy MulAction and for the monodromy homomorphism.
• IsCoveringMap.monodromyPerm_pow_eq_one: over a fibre with d points, the n-th power of every loop class has trivial monodromy whenever d ! divides n.
• IsCoveringMap.exists_monodromy_eq_of_joined, IsCoveringMap.exists_monodromy_eq and IsCoveringMap.monodromy_isPretransitive: monodromy carries a lift to any lift joined to it by a path, so it is transitive on a fibre of a path-connected cover.
• IsCoveringMap.joined_monodromy and IsCoveringMap.pathConnectedSpace_iff: conversely a point is joined to its image under monodromy, so over a path-connected base the total space is path connected exactly when monodromy is transitive on a nonempty fibre.
• IsCoveringMap.fiberEquivQuotientRange and IsCoveringMap.card_fiber_eq_index: the fibre is the coset space of the recovered subgroup, so the number of sheets is its index.
• IsCoveringMap.range_mapOfEq_monodromy, IsCoveringMap.exists_range_eq_map_conj_of_joined and IsCoveringMap.exists_range_eq_map_conj: changing the lift conjugates the recovered subgroup, and on a path-connected cover realises every conjugate.
• IsCoveringMap.normal_range_iff: the recovered subgroup is normal exactly when it is independent of the chosen lift.

References

This is Stage 2 of TauCetiRoadmap/UniversalCovers/README.md: item 7 asks for the subgroup a pointed cover recovers and for the way it transforms when the chosen lift changes, and item 8 splits the classification into a pointed statement about subgroups and an unpointed statement about conjugacy classes, phrased "via transitive π₁(X)-sets". Everything here is built from Junyan Xu's monodromy API in Mathlib/Topology/Homotopy/Lifting.lean; no Mathlib proof is vendored.

Monodromy as a bijection between fibres

theorem IsCoveringMap.coe_monodromy_mk {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {x y : X} (γ : Path x y) (e : ↑(p ⁻¹' {x})) (h : γ.toContinuousMap 0 = p ↑e) : ↑(hp.monodromy (Path.Homotopic.Quotient.mk γ) e) = (hp.liftPath γ.toContinuousMap (↑e) h) 1

Monodromy along the class of a path γ sends a lift e of its source to the endpoint of the lift of γ starting at e. This is the defining formula of IsCoveringMap.monodromy on a representative path.

noncomputable def TauCeti.coveringFiberEquiv {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {x y : X} (γ : Path.Homotopic.Quotient x y) : ↑(p ⁻¹' {x}) ≃ ↑(p ⁻¹' {y})

Monodromy along a homotopy class of paths is a bijection between the fibres over its endpoints. It is IsCoveringMap.monodromy, whose bijectivity Mathlib records, packaged as an equivalence.

Equations

• TauCeti.coveringFiberEquiv hp γ = Equiv.ofBijective (hp.monodromy γ) ⋯

@[simp]

theorem TauCeti.coveringFiberEquiv_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {x y : X} (γ : Path.Homotopic.Quotient x y) (e : ↑(p ⁻¹' {x})) : (coveringFiberEquiv hp γ) e = hp.monodromy γ e

@[simp]

theorem TauCeti.coveringFiberEquiv_symm_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {x y : X} (γ : Path.Homotopic.Quotient x y) (e : ↑(p ⁻¹' {y})) : (coveringFiberEquiv hp γ).symm e = hp.monodromy γ.symm e

The inverse of monodromy along γ is monodromy along the reversed class γ.symm.

theorem IsCoveringMap.toPermHom_eq_monodromyPerm {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) (x : X) : MulAction.toPermHom (FundamentalGroup X x) ↑(p ⁻¹' {x}) = hp.monodromyPerm x

The permutation representation of the monodromy action of π₁(X, x) on the fibre over x is Mathlib's monodromy homomorphism IsCoveringMap.monodromyPerm, which is defined as it.

The recovered subgroup

theorem IsCoveringMap.monodromy_eq_self_iff_mem_range {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (γ : FundamentalGroup X x) : hp.monodromy γ e = e ↔ γ ∈ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

A loop class of the base fixes a chosen lift e of the basepoint under monodromy exactly when it is the image of a loop class of the total space based at e.

The image subgroup on the right is the subgroup of π₁(X, x) that the classification of covers attaches to the pointed cover (E, e).

@[simp]

theorem IsCoveringMap.stabilizer_eq_range {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : MulAction.stabilizer (FundamentalGroup X x) e = (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

The stabiliser of a chosen lift e of the basepoint, for the monodromy action of π₁(X, x) on the fibre over x, is the image of π₁(E, e) under the covering map.

theorem IsCoveringMap.comap_stabilizer_monodromyPerm {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : Subgroup.comap (hp.monodromyPerm x) (MulAction.stabilizer (Equiv.Perm ↑(p ⁻¹' {x})) e) = (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

The preimage under the monodromy homomorphism IsCoveringMap.monodromyPerm of the stabiliser of a chosen lift e of the basepoint is the image of π₁(E, e) under the covering map.

theorem IsCoveringMap.monodromyPerm_pow_eq_one {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} (hp : IsCoveringMap p) [Finite ↑(p ⁻¹' {x})] {n : ℕ} (hn : (Nat.card ↑(p ⁻¹' {x})).factorial ∣ n) (γ : FundamentalGroup X x) : (hp.monodromyPerm x) (γ ^ n) = 1

Over a finite fibre, a suitable power of every loop has trivial monodromy. If the fibre over x has d points and d ! divides n, then the n-th power of every loop class at x acts trivially on that fibre, because the monodromy permutation lies in a group of order d !.

Transitivity on a fibre

theorem IsCoveringMap.exists_monodromy_eq_of_joined {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} (hp : IsCoveringMap p) {e e' : ↑(p ⁻¹' {x})} (h : Joined ↑e ↑e') : ∃ (γ : FundamentalGroup X x), hp.monodromy γ e = e'

A path joining two lifts of the basepoint projects to a loop of the base whose monodromy carries the first lift to the second.

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

On a fibre of a path-connected cover, monodromy is transitive.

theorem IsCoveringMap.monodromy_isPretransitive {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} [PathConnectedSpace E] (hp : IsCoveringMap p) (x : X) : MulAction.IsPretransitive (FundamentalGroup X x) ↑(p ⁻¹' {x})

The monodromy action of π₁(X, x) on a fibre of a path-connected cover is transitive.

theorem IsCoveringMap.joined_monodromy {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {x y : X} (γ : Path.Homotopic.Quotient x y) (e : ↑(p ⁻¹' {x})) : Joined ↑e ↑(hp.monodromy γ e)

A point of a fibre is joined to its image under monodromy, by the lifted path.

theorem IsCoveringMap.pathConnectedSpace_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} [PathConnectedSpace X] (hp : IsCoveringMap p) (x : X) : PathConnectedSpace E ↔ Nonempty ↑(p ⁻¹' {x}) ∧ MulAction.IsPretransitive (FundamentalGroup X x) ↑(p ⁻¹' {x})

A cover of a path-connected space is path connected exactly when monodromy is transitive on a nonempty fibre. Every point of the total space is joined to the fibre over x by lifting a path to x, and two points of that fibre are joined by lifting a loop.

The fibre as a coset space

noncomputable def IsCoveringMap.fiberEquivQuotientRange {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [PathConnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : ↑(p ⁻¹' {x}) ≃ FundamentalGroup X x ⧸ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

Orbit-stabiliser for a covering map. Choosing a lift e of the basepoint identifies the fibre over x with the coset space of the subgroup of π₁(X, x) recovered from (E, e), provided the cover is path connected.

Equations

• hp.fiberEquivQuotientRange e = (Equiv.subtypeUnivEquiv ⋯).symm.trans ((MulAction.orbitEquivQuotientStabilizer (FundamentalGroup X x) e).trans (Subgroup.quotientEquivOfEq ⋯))

@[simp]

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

The inverse of the orbit-stabiliser identification sends the coset of a loop class to the monodromy translate of the chosen lift.

theorem IsCoveringMap.card_fiber_eq_index {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [PathConnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : Nat.card ↑(p ⁻¹' {x}) = (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range.index

The number of sheets of a path-connected cover is the index of the recovered subgroup.

Dependence on the chosen lift

theorem IsCoveringMap.range_mapOfEq_monodromy {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) (γ : FundamentalGroup X x) : (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj γ)) (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

Moving the chosen lift by monodromy conjugates the recovered subgroup.

theorem IsCoveringMap.exists_range_eq_map_conj_of_joined {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} (hp : IsCoveringMap p) {e e' : ↑(p ⁻¹' {x})} (h : Joined ↑e ↑e') : ∃ (γ : FundamentalGroup X x), (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj γ)) (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

Two lifts of the basepoint joined by a path in the cover recover conjugate subgroups.

theorem IsCoveringMap.exists_range_eq_map_conj {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [PathConnectedSpace E] (hp : IsCoveringMap p) (e e' : ↑(p ⁻¹' {x})) : ∃ (γ : FundamentalGroup X x), (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj γ)) (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

On a path-connected cover, any two lifts of the basepoint recover conjugate subgroups: an unpointed connected cover determines only the conjugacy class of the subgroup.

theorem IsCoveringMap.normal_range_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [PathConnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range.Normal ↔ ∀ (e' : ↑(p ⁻¹' {x})), (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range = (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

On a path-connected cover, the subgroup recovered from a lift of the basepoint is normal exactly when it does not depend on which lift is chosen. This is the subgroup-side criterion for the cover to be regular.