Proposition 1.40(a): for a covering space action, $Y\to Y/G$ is a normal covering space

Read-back of Hatcher.orbitProj_isCoveringMap.

Setting and binders

• G Y : Type* — two types in independent, arbitrary universes.
• [Group G] — $G$ is a group (multiplicative notation, identity 1).
• [TopologicalSpace Y].
• [MulAction G Y] — a left action $G\times Y\to Y$, $(g,y)\mapsto g\cdot y$, with $1\cdot y = y$ and $(gh)\cdot y = g\cdot(h\cdot y)$. No continuity is part of MulAction.
• (hGY : IsCoveringSpaceAction G Y) — from the bundle:
  1. for every $g\in G$ the map $y\mapsto g\cdot y$ is continuous (hence a homeomorphism, with inverse $g^{-1}\cdot -$), and
  2. for every $y\in Y$ there is a set $U\in\mathcal N(y)$ (a neighbourhood of $y$: it contains an open set containing $y$, but need not itself be open) such that for all $g\in G$, if $(g\cdot U)\cap U\neq\emptyset$ then $g = 1$. (Precedence check: (fun z => g • z) '' U ∩ U is ((g•·) '' U) ∩ U, since '' binds tighter than ∩.) Condition 2 implies the action is free: if $g\cdot y = y$ then $y \in g U\cap U$, so $g=1$.

Definitions used:

• OrbitSpace G Y — MulAction.orbitRel.Quotient G Y, the quotient of $Y$ by the equivalence relation $a\sim b \iff a\in G\cdot b = \{g\cdot b\}$. Its topology is Mathlib's instance on Quotient: the topology coinduced by Quotient.mk', i.e. the quotient topology ($V\subseteq Y/G$ open iff its preimage in $Y$ is open).
• orbitProj G Y : Y → OrbitSpace G Y — Quotient.mk _, the canonical projection $\pi : y\mapsto [y]$; surjective by construction.
• IsCoveringMap (orbitProj G Y) — Mathlib's predicate: for every $[y]\in Y/G$ the fibre $\pi^{-1}\{[y]\}$ (which as a set is the orbit $G\cdot y$, with the subspace topology from $Y$) is discrete, and there is an open $V\ni[y]$ with $\pi^{-1}(V)$ open and a homeomorphism $\pi^{-1}(V)\cong V\times\pi^{-1}\{[y]\}$ over $V$.
• deckGroup (orbitProj G Y) : Subgroup (Y ≃ₜ Y) — homeomorphisms $f:Y\to Y$ with $\pi(f y)=\pi(y)$ for all $y$, i.e. $f(y)\in G\cdot y$ for every $y$ (orbit-preserving homeomorphisms). Note this depends only on the function $\pi$, not on the topology of $Y/G$.
• IsNormalCover (orbitProj G Y) — $\forall y,y'\in Y,\ \pi(y)=\pi(y')\Rightarrow\exists f\in\mathrm{Deck}(\pi),\ f(y)=y'$: the orbit-preserving homeomorphisms act transitively on each orbit.

Hypotheses

Only hGY: the action is by homeomorphisms and satisfies the local "$gU\cap U\neq\emptyset\Rightarrow g=1$" condition. No connectivity, Hausdorffness, local path-connectedness, or nonemptiness of $Y$ is assumed; no assumption on $G$ beyond being a group.

Conclusion

Both of:

1. $\pi : Y\to Y/G$ is a covering map (Mathlib sense), and
2. $\pi$ is a normal cover: whenever $[y]=[y']$ there is a homeomorphism $f$ of $Y$ with $\pi\circ f=\pi$ and $f(y)=y'$.

Remarks

• Matches Hatcher, Prop. 1.40(a): "the quotient map $p:Y\to Y/G$ is a normal covering space" for a covering space action. Hatcher states (a) without connectivity hypotheses, exactly as here.
• Hatcher's condition (*) asks for an open neighbourhood $U$ with $g_1U\cap g_2U\neq\emptyset\Rightarrow g_1=g_2$. The bundle uses a (not necessarily open) neighbourhood and the one-element form $gU\cap U\neq\emptyset\Rightarrow g=1$; these are equivalent (shrink $U$ to its interior; multiply by $g_2^{-1}$). Hatcher also implicitly assumes $G$ acts by homeomorphisms, which is condition 1 here.
• The IsNormalCover half is essentially immediate from the definitions: if $[y]=[y']$ then $y' = g\cdot y$ for some $g$, and $y\mapsto g\cdot y$ is a homeomorphism (by condition 1) preserving orbits. So the mathematical content lies in the IsCoveringMap half; the conjunction is not misleading, but the second conjunct is weak.
• Edge cases. If $Y=\emptyset$: $Y/G=\emptyset$, IsCoveringMap holds (Mathlib's IsCoveringMap.of_isEmpty), and IsNormalCover is vacuous — the statement is true but trivial. If $G$ is trivial: $\pi$ is a bijection and, with the quotient topology, a homeomorphism; a homeomorphism is a covering map with singleton fibres, and IsNormalCover is trivial. Neither case is excluded.
• orbitProj is surjective by construction, so the "clopen range" subtlety of Mathlib's IsCoveringMap does not arise.
• deckGroup (orbitProj G Y) may be strictly larger than the image of $G$ when $Y$ is disconnected (e.g. $Y$ two points, $G$ trivial: the swap is a deck transformation). This theorem does not claim the deck group is $G$; that is deckGroup_orbitProj, which adds path-connectedness.
• The group $G$ itself (not $G^{\mathrm{op}}$) appears, via the left action; no fundamental groups appear in this statement, so the loop-multiplication convention is irrelevant.
• Universe-polymorphic in G, Y independently.