Proposition 1.39(a): a covering space is normal iff $H=p_*\pi_1(\tilde X,\tilde x_0)$ is a normal subgroup

Read-back of Hatcher.isNormalCover_iff_normal.

Setting and binders

• E X : Type* — two types, each in its own arbitrary universe (no relation between the universes is imposed).
• [TopologicalSpace E] [TopologicalSpace X] — topologies on both.
• [PathConnectedSpace X] — Mathlib's class: Nonempty X and for all $x, y \in X$ there is a continuous path from $x$ to $y$ (Joined x y). In particular $X \neq \emptyset$.
• [LocallyPathConnectedSpace X] — for every $x \in X$ the neighbourhood filter $\mathcal N(x)$ has a basis consisting of sets $s$ with $s \in \mathcal N(x)$ and $s$ path-connected (IsPathConnected s). Equivalent to the usual "locally path-connected".
• [PathConnectedSpace E] — $E$ nonempty and path-connected.
• {p : E → X} — an arbitrary function (implicit).
• (hp : IsCoveringMap p) — Mathlib's covering-map predicate: for every $x \in X$, IsEvenlyCovered p x (p ⁻¹' {x}), i.e. the fibre $p^{-1}\{x\}$ (subspace topology) is discrete, and there is an open $U \ni x$ with $p^{-1}(U)$ open and a homeomorphism $H : p^{-1}(U) \cong U \times p^{-1}\{x\}$ whose first coordinate is $p$. Surjectivity is not built in: for $x \notin p(E)$ the condition says $x$ has an open neighbourhood $U$ with $p^{-1}(U)=\emptyset$; hence $p(E)$ is clopen. Here, since $E \neq \emptyset$ and $X$ is connected, $p$ is in fact surjective, but that is a consequence, not a hypothesis. hp.continuous : Continuous p is derived from hp.
• {e₀ : E} {x₀ : X} (he : p e₀ = x₀) — a base point in $E$ and its image in $X$.

Definitions from the bundle that occur:

• deckGroup p : Subgroup (E ≃ₜ E) — the subgroup of the group of self-homeomorphisms of $E$ with carrier $\{f : E \cong E \mid \forall e,\ p(f e) = p e\}$. The group law on E ≃ₜ E is mul f g := g.trans f, so $(f g)(e) = f(g(e))$, $1 = \mathrm{id}$, $f^{-1} = f^{\mathrm{symm}}$. This is defined for any function $p$; it does not use continuity of $p$.
• IsNormalCover p : Prop — $\forall e, e' \in E,\ p e = p e' \Rightarrow \exists f \in \mathrm{deckGroup}\,p,\ f e = e'$. In words: the deck group acts transitively on every fibre of $p$. Again defined for any function $p$.
• coverHom p hp he : FundamentalGroup E e₀ →* FundamentalGroup X x₀ — FundamentalGroup.mapOfEq ⟨p, hp⟩ he, the induced homomorphism $p_* : \pi_1(E,e_0) \to \pi_1(X,x_0)$ (with the identification $p(e_0) = x_0$ built in by he).
• coverSubgroup p hp he : Subgroup (FundamentalGroup X x₀) — (coverHom p hp he).range, i.e. $H := p_*\pi_1(E,e_0) \le \pi_1(X,x_0)$.
• FundamentalGroup X x₀ — Mathlib's $\pi_1$: End (FundamentalGroupoid.mk x₀), homotopy classes (rel endpoints) of loops at $x_0$. Its multiplication is x * y := y ≫ x, and ≫ is Path.Homotopic.Quotient.trans, so $[\gamma]\cdot[\delta] = [\delta \ast \gamma]$ ("first $\delta$, then $\gamma$") — the opposite of Hatcher's convention $[\gamma][\delta]=[\gamma\cdot\delta]$. Normality of a subgroup is the same in a group and its opposite, so this does not affect the statement.
• Subgroup.Normal H — ∀ n, n ∈ H → ∀ g, g * n * g⁻¹ ∈ H.

Hypotheses

$X$ nonempty, path-connected, locally path-connected; $E$ nonempty, path-connected; $p : E \to X$ a covering map in Mathlib's sense; $e_0 \in E$ with $p(e_0) = x_0$.

Conclusion

Left side: for every pair of points in the same fibre there is a homeomorphism $f : E \to E$ commuting with $p$ (a deck transformation) carrying one to the other. Right side: the image subgroup $H = p_*\pi_1(E,e_0)$ is closed under conjugation by every element of $\pi_1(X,x_0)$.

Remarks

• This matches Hatcher, Prop. 1.39(a): for a path-connected covering space $p : (\tilde X, \tilde x_0) \to (X, x_0)$ of a path-connected, locally path-connected $X$, the covering is normal iff $H = p_*(\pi_1(\tilde X,\tilde x_0))$ is normal in $\pi_1(X,x_0)$. Hatcher's definition of "normal covering" ("for each pair of lifts of each $x$ there is a deck transformation taking one to the other") is literally IsNormalCover p.
• Deck transformations are required to be homeomorphisms (E ≃ₜ E), as in the textbook; the condition $p\circ f = p$ is imposed pointwise.
• Nothing is vacuous: PathConnectedSpace E forces $E \ne \emptyset$; combined with connectedness of $X$ and the clopen range, $p$ is surjective, so every fibre is nonempty.
• The left side quantifies over all fibres, whereas the right side is about a single base point $x_0$; this is the standard formulation and the hypotheses make the base point irrelevant.
• The only role of x₀ is through he; the statement is really about $e_0$ and $p(e_0)$.
• No Hausdorff, second-countability, or semilocal simple-connectivity is assumed or needed.
• Universe-wise, E and X may live in different universes; the statement is fully universe-polymorphic.
• Under SimplyConnectedSpace E the right side is automatic ($H$ trivial), and the left side then asserts the universal cover is normal — consistent with the textbook.