Unpointed connected covers are determined by a conjugacy class of subgroups

Choosing a point in the fibre of a connected covering map over x recovers a subgroup of FundamentalGroup X x. The pointed classification theorem says that two covers with chosen fibre points are isomorphic over X precisely when these subgroups are equal. Without chosen fibre points, equality is replaced by conjugacy: moving a fibre point by monodromy conjugates the recovered subgroup, and every fibre point is reached by monodromy.

This file combines those two facts. For path-connected, locally path-connected covering spaces E and F, it proves that there is a homeomorphism E ≃ₜ F over X if and only if the subgroups recovered from any chosen lifts e₀ and f₀ are conjugate in π₁(X, x). The conjugacy convention is written explicitly as

range(q, f₀) = range(p, e₀).map (MulAut.conj γ).toMonoidHom.

The statement does not need connectedness, local connectedness, or semilocal simple connectedness of the base. Those hypotheses are needed to construct a cover from every subgroup, not to compare two covers which already exist.

Main declarations

• IsCoveringMap.exists_range_eq_map_conj_of_homeomorph_comp_eq: an isomorphism of unpointed covers makes their recovered subgroups conjugate, as soon as h e₀ and f₀ are joined by a path.
• IsCoveringMap.exists_homeomorph_comp_eq_of_range_eq_map_conj: conjugate recovered subgroups give an isomorphism of unpointed covers.
• IsCoveringMap.exists_homeomorph_comp_eq_iff_exists_range_eq_map_conj: the unpointed connected-cover comparison theorem.

References

This advances TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 8, second bullet: unpointed connected covers correspond to conjugacy classes of subgroups. It proves the comparison-up-to-isomorphism half of that correspondence; constructing a cover from every subgroup is the separate existence milestone in item 7.

The proof reuses IsCoveringMap.exists_homeomorph_comp_eq_iff_range_eq for pointed covers and IsCoveringMap.exists_range_eq_map_conj for change of the chosen lift. The latter is built on Junyan Xu's monodromy API in Mathlib.Topology.Homotopy.Lifting; no external formalization is copied or adapted here.

theorem IsCoveringMap.exists_range_eq_map_conj_of_homeomorph_comp_eq {E : Type u_1} {F : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {x : X} {e₀ : E} {f₀ : F} (hq : IsCoveringMap q) (hpe : p e₀ = x) (hqf : q f₀ = x) (h : E ≃ₜ F) (hcomp : q ∘ ⇑h = p) (hj : Joined (h e₀) f₀) : ∃ (γ : FundamentalGroup X x), (FundamentalGroup.mapOfEq { toFun := q, continuous_toFun := ⋯ } hqf).range = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj γ)) (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } hpe).range

An isomorphism of unpointed covers carries the subgroup recovered from the source basepoint to a conjugate of the subgroup recovered from the target basepoint, provided h e₀ and f₀ are joined by a path.

The homeomorphism need not carry e₀ to f₀: its image of e₀ is another point of the target fibre, and a path from there to f₀ is what accounts for the conjugation.

Neither cover is assumed connected. Path-connectedness of F is one way to supply hj, and is how IsCoveringMap.exists_homeomorph_comp_eq_iff_exists_range_eq_map_conj below discharges it.

theorem IsCoveringMap.exists_homeomorph_comp_eq_of_range_eq_map_conj {E : Type u_1} {F : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {x : X} {e₀ : E} {f₀ : F} [PathConnectedSpace E] [LocallyPathConnectedSpace E] [PathConnectedSpace F] [LocallyPathConnectedSpace F] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (hpe : p e₀ = x) (hqf : q f₀ = x) (γ : FundamentalGroup X x) (hrange : (FundamentalGroup.mapOfEq { toFun := q, continuous_toFun := ⋯ } hqf).range = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj γ)) (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } hpe).range) : ∃ (h : E ≃ₜ F), q ∘ ⇑h = p

If two pointed connected covers recover conjugate subgroups, then forgetting the chosen fibre points makes the covers isomorphic over the base.

theorem IsCoveringMap.exists_homeomorph_comp_eq_iff_exists_range_eq_map_conj {E : Type u_1} {F : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {x : X} {e₀ : E} {f₀ : F} [PathConnectedSpace E] [LocallyPathConnectedSpace E] [PathConnectedSpace F] [LocallyPathConnectedSpace F] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (hpe : p e₀ = x) (hqf : q f₀ = x) : (∃ (h : E ≃ₜ F), q ∘ ⇑h = p) ↔ ∃ (γ : FundamentalGroup X x), (FundamentalGroup.mapOfEq { toFun := q, continuous_toFun := ⋯ } hqf).range = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj γ)) (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } hpe).range

Unpointed connected covers are classified up to isomorphism by the conjugacy class of the subgroup they recover. There is a homeomorphism of the total spaces over X exactly when the subgroups recovered from chosen lifts of x are conjugate in π₁(X, x).

The chosen lifts occur only in the subgroup invariant; the homeomorphism is not required to map one chosen lift to the other.