Proposition 1.39(b): $G(\tilde X)\cong N(H)/H$

Read-back of Hatcher.exists_normalizer_hom_deckGroup.

Setting and binders

• E X : Type* — two types in independent, arbitrary universes.
• [TopologicalSpace E] [TopologicalSpace X].
• [PathConnectedSpace X] — $X$ is nonempty and any two points are joined by a continuous path.
• [LocallyPathConnectedSpace X] — each neighbourhood filter $\mathcal N(x)$ has a basis of path-connected neighbourhoods.
• [PathConnectedSpace E] — $E$ nonempty and path-connected.
• {p : E → X} and (hp : IsCoveringMap p) — Mathlib's covering-map predicate: every $x\in X$ has an open neighbourhood $U$ such that $p^{-1}(U)$ is open and homeomorphic over $U$ to $U \times p^{-1}\{x\}$, with $p^{-1}\{x\}$ discrete. Surjectivity is not part of the definition (points outside the range must have a neighbourhood with empty preimage), but here it follows from $E\neq\emptyset$ and $X$ connected.
• {e₀ : E} {x₀ : X} (he : p e₀ = x₀).

Definitions used:

• FundamentalGroup X x₀ — $\pi_1(X,x_0)$, homotopy classes of loops at $x_0$; multiplication [γ] * [δ] = [δ.trans γ] (reverse of Hatcher's order; see Remarks).
• coverSubgroup p hp.continuous he — $H := p_*\pi_1(E,e_0) \le \pi_1(X,x_0)$, the range of the induced homomorphism FundamentalGroup.mapOfEq ⟨p, hp.continuous⟩ he.
• (coverSubgroup … : Set (FundamentalGroup X x₀)) — the underlying set of $H$; Subgroup.normalizer takes a Set.
• Subgroup.normalizer S — the subgroup $\{g \mid \forall n,\ n \in S \iff g n g^{-1} \in S\}$. For $S = H$ a subgroup this is $N(H) = \{g \mid gHg^{-1} = H\}$, the usual normalizer. Below N := Subgroup.normalizer (H : Set _), and N is also used for its coercion to a type (elements are pairs $\langle g, g\in N\rangle$) with the induced group structure.
• deckGroup p : Subgroup (E ≃ₜ E) — homeomorphisms $f : E \to E$ with $p(f e) = p e$ for all $e$; group law $(fg)(e) = f(g(e))$. Coerced to a type with its group structure.
• φ : N →* deckGroup p — a group homomorphism (bundled MonoidHom).
• Function.Surjective φ — $\forall d \in \mathrm{deckGroup}\,p,\ \exists n \in N,\ \varphi(n) = d$.
• φ.ker : Subgroup N — $\{n \in N \mid \varphi(n) = 1\}$, where $1$ is the identity homeomorphism.
• H.subgroupOf N : Subgroup N — H.comap N.subtype, i.e. $\{n \in N \mid (n : \pi_1(X,x_0)) \in H\}$: "$H$ regarded as a subgroup of $N$" (note $H \le N(H)$ always, so this is a copy of $H$ inside $N$).

Hypotheses

$X$ path-connected and locally path-connected (hence nonempty); $E$ path-connected (hence nonempty); $p$ a covering map; $p(e_0)=x_0$.

Conclusion

There exists a group homomorphism

such that

1. $\varphi$ is surjective, and
2. $\ker\varphi = H$ (more precisely, $\ker\varphi$ equals the subgroup of $N(H)$ consisting of those elements that lie in $H$; as subgroups of the type $N(H)$, φ.ker = H.subgroupOf N(H)).

By the first isomorphism theorem this is equivalent to the assertion

i.e. the quotient of the normalizer of $H$ by $H$ is isomorphic (as an abstract group) to the deck transformation group. Conversely, any such isomorphism composed with the projection $N(H)\to N(H)/H$ yields a $\varphi$ as required, so the Lean statement and the quotient-isomorphism statement are logically equivalent.

Remarks

• Matches Hatcher, Prop. 1.39(b): $G(\tilde X) \cong N(H)/H$ for a path-connected covering of a path-connected, locally path-connected base.
• Only existence is asserted. The theorem does not say that $\varphi$ is the canonical map (sending $[\gamma]\in N(H)$ to the deck transformation taking $e_0$ to the endpoint of the lift of $\gamma$ at $e_0$), nor that $\varphi$ is compatible with any lifting. Any surjective homomorphism with the right kernel satisfies it.
• Direction. The map goes from the normalizer to the deck group, as in Hatcher; the deck group is the target, and surjectivity is the "every deck transformation arises from a loop" half.
• Opposite-group issue. Mathlib's $\pi_1$ multiplies loops in the reverse order to Hatcher's. Since composing any homomorphism $\psi : G^{\mathrm{op}} \to D$ with inversion $g\mapsto g^{-1}$ produces a homomorphism $G\to D$ with the same image and kernel, existence of $\varphi$ is insensitive to this convention; and $N(H)$ and $H$ are the same subsets in $G$ and $G^{\mathrm{op}}$. So no mismatch, but a reader checking a specific formula for $\varphi$ against Hatcher would have to reverse products.
• The deck group uses the composition convention $(fg)(e) = f(g(e))$, so deckGroup p is the deck group with its standard (not opposite) structure.
• Nonvacuous: PathConnectedSpace E and PathConnectedSpace X give nonempty spaces; $p$ is surjective, so deckGroup and H are the textbook objects. If $E$ were empty the statement could not even be formed (no e₀).
• Special cases: if $H$ is normal (equivalently, by the companion theorem, IsNormalCover p), then $N(H) = \pi_1(X,x_0)$ and the statement gives $\pi_1(X,x_0)/H\cong\mathrm{Deck}(p)$. If $E$ is simply connected, $H=1$, $N(H)=\pi_1(X,x_0)$, and $\varphi$ is an isomorphism $\pi_1(X,x_0)\cong\mathrm{Deck}(p)$ (this is the content of deckGroup_equiv_fundamentalGroup).
• No Hausdorff or separation hypotheses. Universe-polymorphic in E, X independently.