Change of basepoint in the fibre conjugates $p_*\pi_1(\tilde X,\tilde x_0)$, and every conjugate arises

Read-back of Hatcher.coverSubgroup_conj.

Setting and binders

• {E X : Type*} — two types in independent, arbitrary universes (this theorem does not go through the CoveringSpace structure, so no universe sharing is imposed).
• [TopologicalSpace E] [TopologicalSpace X] — topologies on both.
• [PathConnectedSpace E] — the total space E is nonempty and any two of its points are joined by a path. Note: this is on E, not X; no hypothesis at all is placed on X (not path-connected, not locally path-connected, not semilocally simply-connected).
• {p : E → X}, hp : IsCoveringMap p — p is a covering map in Mathlib's sense: every x : X has an open neighbourhood U with p⁻¹(U) open and p⁻¹(U) ≃ₜ U × p⁻¹{x} over U, with p⁻¹{x} discrete. No surjectivity is built in. hp.continuous : Continuous p is used to form the induced homomorphisms.
• {x₀ : X}, {e₀ : E}, he₀ : p e₀ = x₀ — a basepoint e₀ in the fibre over x₀.

For any e : E with he : p e = x₀, write

$$H_e := \texttt{coverSubgroup } p\ hp.\texttt{continuous}\ he = \operatorname{range}\big(\texttt{FundamentalGroup.mapOfEq}\,\langle p, hp.\texttt{continuous}\rangle\, he\big) = p_*\big(\pi_1(E,e)\big) \le \pi_1(X,x_0).$$

By Mathlib's mapOfEq_apply, the homomorphism sends the class of a loop γ at e to the class of p ∘ γ, re-indexed to be a loop at x₀ via p e = x₀; so $H_e$ is the honest image of $\pi_1(E,e)$ under $p_*$. Note coverSubgroup takes the proof he as an argument, so different points e₁ of the fibre give (a priori) different subgroups $H_{e_1}$, all inside the single group FundamentalGroup X x₀.

The conjugation operator. For g : FundamentalGroup X x₀, MulAut.conj g : MulAut G is the automorphism h ↦ g * h * g⁻¹ (Mathlib MulAut.conj_apply, definitionally), and .toMonoidHom views it as a group homomorphism. Subgroup.map φ H has carrier φ '' H (Subgroup.mem_map : y ∈ H.map φ ↔ ∃ x ∈ H, φ x = y). Therefore

$$H.\texttt{map}\,(\texttt{MulAut.conj } g).\texttt{toMonoidHom} = \{\, g * h * g^{-1} : h\in H\,\} = gHg^{-1}$$

with respect to Mathlib's multiplication on FundamentalGroup, which is p * q = q.trans p (traverse q first, then p). In Hatcher's concatenation-order product $[\alpha][\beta]=[\alpha\cdot\beta]$, Mathlib's g * h * g⁻¹ is $g^{-1}\cdot h\cdot g$. So the Lean expression is "$gHg^{-1}$" in Lean's group law and "$g^{-1}Hg$" in Hatcher's notation. Since in both conjuncts g is bound by an existential or universal quantifier ranging over the whole group, this convention does not change the mathematical content of the theorem.

Hypotheses

Exactly: E path-connected, p a covering map, p e₀ = x₀. No hypotheses on X.

Conclusion

A conjunction of two statements.

(a) For every e₁ : E and every proof he₁ : p e₁ = x₀ (i.e. every point of the fibre $p^{-1}(x_0)$),

$$\exists\, g\in\pi_1(X,x_0):\quad g\,H_{e_0}\,g^{-1} = H_{e_1}.$$

In words: the subgroup attached to any other basepoint in the fibre is a conjugate of the one attached to e₀.

(b) For every g : FundamentalGroup X x₀,

$$\exists\, e_1\in E,\ \exists\, he_1 : p(e_1) = x_0:\quad g\,H_{e_0}\,g^{-1} = H_{e_1}.$$

In words: every conjugate of $H_{e_0}$ is realised as the subgroup attached to some basepoint in the fibre over x₀.

Together: the set $\{H_{e} : e\in p^{-1}(x_0)\}$ is exactly the conjugacy class of $H_{e_0}$ in $\pi_1(X,x_0)$. This is Hatcher, Proposition 1.39 ("changing the basepoint $\tilde x_0$ within $p^{-1}(x_0)$ corresponds exactly to changing $H$ to a conjugate subgroup") — including the "exactly" (every conjugate occurs).

Remarks

1. Not vacuous. E path-connected gives Nonempty E, and e₀ is given, so the fibre over x₀ is nonempty; the quantifiers in (a) range over a nonempty set. The hypotheses are satisfiable by any path-connected covering (e.g. $\mathbb R\to S^1$).
2. Trivial instances. If E is simply connected, all $H_e = \{1\}$ and both conjuncts are trivially true; if $\pi_1(X,x_0)$ is trivial, g = 1 is the only element and (a),(b) reduce to $H_{e_0}=H_{e_1}=\{1\}$. These are consistent with the textbook, not defects.
3. Where the hypotheses are used (as stated, not as proved). (a) is the direction that needs E path-connected (a path in E from e₀ to e₁ projects to a loop g). (b) only needs path-lifting from e₀, which holds for any covering map with e₀ in the fibre; the theorem nevertheless assumes path-connectedness globally. No local path-connectedness of X or E is needed for either direction, and none is assumed.
4. No hypothesis on X; p need not be surjective onto X. The statement is only about the fibre over the single point x₀, so surjectivity is irrelevant; X may be disconnected, and p may miss other components of X entirely.
5. Existence over a proof. ∃ he₁ : p e₁ = x₀, … quantifies over a proof of a Prop; by proof irrelevance this is the same as p e₁ = x₀ ∧ ….
6. Exact conjugate. As computed above, the Lean expression H.map (MulAut.conj g).toMonoidHom is $gHg^{-1}$ in Mathlib's product, i.e. $g^{-1}Hg$ in Hatcher's. Hatcher's proof gives $H_{e_1} = [\gamma]^{-1}H_{e_0}[\gamma]$ (his convention) for $\gamma$ the projection of a path from $\tilde x_0$ to $\tilde x_1$, which is $[\gamma] H_{e_0}[\gamma]^{-1}$ in Mathlib's product; the formal statement does not pin down which g, only that some g works, so no direction mismatch can arise.
7. Universes. E and X are fully polymorphic here, unlike the CoveringSpace-based theorems.
8. Nothing a textbook statement would normally contain is absent; the theorem does not name the conjugating element in terms of a path (Hatcher does in the proof, not the proposition).