Basepoint change for the subgroup recovered by a cover

Let p : E → X be a covering map, let γ : Path x₀ x₁, and let e₀ lie over x₀. The lifted endpoint hp.monodromy ⟦γ⟧ e₀ lies over x₁, and the subgroup recovered from that pointed lift is the transport of the subgroup recovered from e₀ along γ:

  im (p_* : π₁(E, hp.monodromy ⟦γ⟧ e₀) → π₁(X, x₁))
    = γ_* (im (p_* : π₁(E, e₀) → π₁(X, x₀))).

Here p_* denotes the induced map on fundamental groups and γ_* denotes the basepoint-change isomorphism induced by γ; the displayed equality is an equality of image subgroups.

The proof combines Mathlib's path-conjugation isomorphism for fundamental groups with its path-lifting and monodromy API, packaged for recovered subgroups in TauCeti.Topology.Homotopy.Monodromy.Basic. This is the path-level compatibility needed by the pointed and unpointed parts of Stage 2, items 7 and 8, of TauCetiRoadmap/UniversalCovers/README.md; the convention is the usual one from Hatcher, Algebraic Topology, Section 1.3.

theorem IsCoveringMap.monodromy_fundamentalGroupMulEquivOfPath_symm_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x₀ x₁ : X} (hp : IsCoveringMap p) (γ : Path x₀ x₁) (g : FundamentalGroup X x₁) (e₀ : ↑(p ⁻¹' {x₀})) : hp.monodromy ((FundamentalGroup.fundamentalGroupMulEquivOfPath γ).symm g) e₀ = (TauCeti.coveringFiberEquiv hp (Path.Homotopic.Quotient.mk γ)).symm (hp.monodromy g (hp.monodromy (Path.Homotopic.Quotient.mk γ) e₀))

Monodromy after basepoint change. Monodromy along the transport back along γ of a loop class g at x₁ is monodromy along g, conjugated by monodromy along γ: lift γ, then go around g, then return along γ.

theorem IsCoveringMap.monodromyPerm_fundamentalGroupMulEquivOfPath_symm {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x₀ x₁ : X} (hp : IsCoveringMap p) (γ : Path x₀ x₁) (g : FundamentalGroup X x₁) : (hp.monodromyPerm x₀) ((FundamentalGroup.fundamentalGroupMulEquivOfPath γ).symm g) = (TauCeti.coveringFiberEquiv hp (Path.Homotopic.Quotient.mk γ)).symm.permCongr ((hp.monodromyPerm x₁) g)

The monodromy permutation of the transport back along γ of a loop class g is the monodromy permutation of g, transported from the fibre over x₁ to the fibre over x₀ by monodromy along γ.

theorem IsCoveringMap.monodromy_eq_self_iff_fundamentalGroupMulEquivOfPath_symm_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x₀ x₁ : X} (hp : IsCoveringMap p) (γ : Path x₀ x₁) (e₀ : ↑(p ⁻¹' {x₀})) (g : FundamentalGroup X x₁) : hp.monodromy g (hp.monodromy ⟦γ⟧ e₀) = hp.monodromy ⟦γ⟧ e₀ ↔ hp.monodromy ((FundamentalGroup.fundamentalGroupMulEquivOfPath γ).symm g) e₀ = e₀

Conjugation law for monodromy along a path. A class g at x₁ fixes the endpoint hp.monodromy ⟦γ⟧ e₀ of the lift of γ exactly when its transport back along γ fixes the starting point e₀. This is the path-level statement behind IsCoveringMap.range_mapOfEq_monodromy_path: transporting the recovered subgroup along γ amounts to conjugating the classes that the monodromy action fixes.

theorem IsCoveringMap.range_mapOfEq_monodromy_path {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x₀ x₁ : X} (hp : IsCoveringMap p) (γ : Path x₀ x₁) (e₀ : ↑(p ⁻¹' {x₀})) : (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range = FundamentalGroup.basepointChangeSubgroup γ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

The subgroup recovered at the endpoint of a lifted path is the basepoint transport of the subgroup recovered at its starting point.