Proposition 1.40(b): $G$ is the deck transformation group of $Y\to Y/G$ when $Y$ is path-connected

Read-back of Hatcher.deckGroup_orbitProj.

Setting and binders

• G Y : Type* — independent, arbitrary universes.
• [Group G], [TopologicalSpace Y], [MulAction G Y] — a group $G$ acting on the left on a topological space $Y$: $1\cdot y=y$, $(gh)\cdot y=g\cdot(h\cdot y)$. Continuity is not part of MulAction.
• [PathConnectedSpace Y] — $Y$ is nonempty and any two points are joined by a path.
• (hGY : IsCoveringSpaceAction G Y) — (1) each $y\mapsto g\cdot y$ is continuous (hence a homeomorphism with inverse $g^{-1}\cdot-$); (2) every $y$ has a neighbourhood $U\in\mathcal N(y)$ with $(g\cdot U)\cap U\neq\emptyset\Rightarrow g=1$ for all $g$. Condition (2) implies the action is free.

Definitions used:

• OrbitSpace G Y — the quotient $Y/G$ of $Y$ by $a\sim b\iff a\in G\cdot b$, with the quotient (coinduced) topology.
• orbitProj G Y : Y → Y/G — the canonical projection $\pi(y)=[y]$.
• deckGroup (orbitProj G Y) : Subgroup (Y ≃ₜ Y) — $\mathrm{Deck}(\pi)=\{f\in\mathrm{Homeo}(Y)\mid\forall y,\ \pi(f y)=\pi(y)\}$, i.e. homeomorphisms $f$ of $Y$ such that $f(y)$ lies in the orbit of $y$ for every $y$. Group law: $(fg)(y)=f(g(y))$, $1=\mathrm{id}$, $f^{-1}=$ inverse homeomorphism. Coerced to a type with the induced group structure; its elements are pairs $\langle f, \text{proof}\rangle$ and (φ g : Y ≃ₜ Y) extracts the homeomorphism $f$.
• G ≃* deckGroup (orbitProj G Y) — a MulEquiv: a bijection $G\to\mathrm{Deck}(\pi)$ preserving multiplication, i.e. a group isomorphism.

Hypotheses

$Y$ nonempty and path-connected; $G$ acts on $Y$ by homeomorphisms as a covering space action. No local path-connectedness, Hausdorffness, or assumption on $G$.

Conclusion

There exists a group isomorphism $\varphi : G\xrightarrow{\ \sim\ }\mathrm{Deck}(\pi)$ such that for every $g\in G$ and $y\in Y$,

Since the equation determines $\varphi(g)$ as a homeomorphism (and hence as an element of the subgroup, membership proofs being irrelevant), the statement is equivalent to the conjunction of:

1. for every $g$, the translation $\tau_g : y\mapsto g\cdot y$ is a homeomorphism of $Y$ satisfying $\pi\circ\tau_g=\pi$ (so $\tau_g\in\mathrm{Deck}(\pi)$);
2. $g\mapsto\tau_g$ is a group homomorphism $G\to\mathrm{Deck}(\pi)$ — automatic from the action axioms and the composition convention $(fg)(y)=f(g(y))$, since $\tau_{gh}(y)=g\cdot(h\cdot y)=\tau_g(\tau_h(y))$;
3. $g\mapsto\tau_g$ is injective (the action is faithful: $\tau_g=\mathrm{id}\Rightarrow g=1$);
4. $g\mapsto\tau_g$ is surjective: every homeomorphism $f$ of $Y$ with $f(y)\in G\cdot y$ for all $y$ is of the form $f=\tau_g$ for a single $g\in G$.

Remarks

• Matches Hatcher, Prop. 1.40(b): "$G$ is the group of deck transformations of the covering space $Y\to Y/G$ if $Y$ is path-connected." Hatcher's proof identifies $G$ with the deck group via $g\mapsto\tau_g$, exactly the map pinned down here.
• Unlike the theorems about $\pi_1$, the isomorphism here is explicit: the statement is not merely "$G\cong\mathrm{Deck}(\pi)$ abstractly" but "the natural map $g\mapsto(y\mapsto g\cdot y)$ is an isomorphism". This is stronger than an abstract Nonempty (G ≃* …) and is the textbook content.
• $G$ vs. $G^{\mathrm{op}}$. Because Mathlib's Homeomorph group has $(fg)=f\circ g$ and MulAction is a left action, $g\mapsto\tau_g$ is a genuine homomorphism from $G$ (not from $G^{\mathrm{op}}$). Had the group law on Y ≃ₜ Y been $g\circ f$, this statement would be false in general (it would need $G^{\mathrm{op}}$). The conventions are consistent.
• Path-connectedness is essential for item 4, and it is present. Without it the statement fails: e.g. $Y=\{a,b\}$ discrete, $G=1$; then $\mathrm{Deck}(\pi)=\mathrm{Homeo}(Y)\cong\mathbb Z/2\not\cong G$.
• Edge cases. $G$ trivial, $Y$ path-connected: $\pi$ is a homeomorphism, $\mathrm{Deck}(\pi)=\{f\mid f(y)=y\ \forall y\}=\{\mathrm{id}\}$, and $\varphi$ is the trivial isomorphism — true. $Y$ empty is excluded by PathConnectedSpace Y. Item 3 (injectivity) is guaranteed by hGY (freeness); if hGY were dropped, a non-faithful action would make the statement false, so the hypothesis is doing work.
• The deck group is defined from the function $\pi$ only; the topology on $Y/G$ plays no role in the statement (it does in the neighbouring orbitProj_isCoveringMap).
• No claim is made here that $\pi$ is a covering map; that is a separate theorem. This statement is purely about which orbit-preserving homeomorphisms exist.
• Universe-polymorphic in G, Y independently.