Proposition 1.40(c): $G\cong\pi_1(Y/G)/p_*\pi_1(Y)$

Read-back of Hatcher.fundamentalGroup_orbitSpace.

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$.
• [PathConnectedSpace Y] — $Y$ nonempty and path-connected.
• [LocallyPathConnectedSpace Y] — every neighbourhood filter in $Y$ has a basis of path-connected neighbourhoods. (Assumed for $Y$, not for $Y/G$.)
• (hGY : IsCoveringSpaceAction G Y) — each $y\mapsto g\cdot y$ is continuous, and every $y$ has a neighbourhood $U$ with $(g\cdot U)\cap U\neq\emptyset\Rightarrow g=1$.
• (y₀ : Y) — a base point in $Y$.

Definitions used:

• OrbitSpace G Y — $Y/G$, the quotient of $Y$ by $a\sim b\iff a\in G\cdot b$, with the quotient (coinduced) topology.
• orbitProj G Y — the projection $\pi:Y\to Y/G$, $y\mapsto[y]$; surjective.
• continuous_orbitProj G Y : Continuous (orbitProj G Y) — continuity of $\pi$ (proved in the bundle by continuous_quotient_mk').
• (rfl : orbitProj G Y y₀ = orbitProj G Y y₀) — the trivial proof that $\pi(y_0)=\pi(y_0)$; it plays the role of he in coverSubgroup, so the base point downstairs is exactly $[y_0]$.
• FundamentalGroup (OrbitSpace G Y) (orbitProj G Y y₀) — $\pi_1(Y/G,[y_0])$, homotopy classes of loops at $[y_0]$ in the quotient topology. Mathlib's product is $[\gamma]\cdot[\delta]=[\delta\ast\gamma]$ (reverse of Hatcher's order).
• coverSubgroup (orbitProj G Y) (continuous_orbitProj G Y) rfl : Subgroup (π₁(Y/G,[y₀])) — the range of the induced homomorphism FundamentalGroup.mapOfEq ⟨π, continuous⟩ rfl : π₁(Y,y₀) →* π₁(Y/G,[y₀]), i.e. $H:=\pi_*\pi_1(Y,y_0)$.
• φ : π₁(Y/G,[y₀]) →* G — a group homomorphism.
• Function.Surjective φ — $\forall g\in G,\ \exists c,\ \varphi(c)=g$.
• φ.ker — $\{c\in\pi_1(Y/G,[y_0])\mid\varphi(c)=1\}$; compared as subgroups of $\pi_1(Y/G,[y_0])$ with $H$.

Hypotheses

$Y$ path-connected (nonempty) and locally path-connected; $G$ acts by homeomorphisms as a covering space action; $y_0\in Y$.

Conclusion

There exists a group homomorphism

which is surjective and whose kernel is exactly $H=\pi_*\pi_1(Y,y_0)$.

By the first isomorphism theorem this is equivalent to

the quotient of the fundamental group of the orbit space by the image of the fundamental group of $Y$ is isomorphic to $G$. (Conversely such an isomorphism composed with the quotient projection gives a $\varphi$ as required, so the two formulations are equivalent.) In particular $H$ is a normal subgroup of $\pi_1(Y/G,[y_0])$, which is implied by the statement (kernels are normal).

Remarks

• Matches Hatcher, Prop. 1.40(c): "$G$ is isomorphic to $\pi_1(Y/G)/p_*(\pi_1(Y))$ if $Y$ is path-connected and locally path-connected." Hatcher's isomorphism goes the other way as an iso of quotient with $G$; here it is packaged as a surjection $\pi_1(Y/G)\to G$ with kernel $H$, which is equivalent.
• Only existence of $\varphi$ is asserted. The canonical map (send $[\gamma]$ to the unique $g$ with $g\cdot y_0=\tilde\gamma(1)$, $\tilde\gamma$ the lift of $\gamma$ at $y_0$) is not specified; any surjective homomorphism with kernel $H$ satisfies the statement.
• Direction and group vs. opposite. The map goes from $\pi_1$ to $G$ (matching the textbook's $\pi_1(Y/G)\to G$). With Mathlib's reversed loop product, the canonical map is a homomorphism from $\pi_1^{\mathrm{Mathlib}}$ only after composing with inversion in $G$ or in $\pi_1$; but composing with inversion preserves surjectivity and kernel, so the existence statement holds under either convention. No mismatch, but a reader comparing an explicit formula to Hatcher must reverse products.
• The base point in the quotient is exactly $[y_0]$ via the rfl argument; there is no hidden change of base point.
• Local path-connectedness is assumed on $Y$; Hatcher assumes it on $Y$ too ($Y/G$ inherits it since $\pi$ is open). Path-connectedness of $Y/G$ follows from that of $Y$ (continuous surjective image).
• Edge cases. $G$ trivial: $\pi$ is a homeomorphism, $H=\pi_1(Y/G,[y_0])$, and $\varphi$ is the trivial map with full kernel — true. $Y$ simply connected: $H=1$ and the statement gives $\pi_1(Y/G,[y_0])\cong G$ (e.g. $\mathbb Z$ acting on $\mathbb R$, $\pi_1(S^1)\cong\mathbb Z$). $Y$ empty is excluded by PathConnectedSpace Y. The statement is never vacuous.
• The IsCoveringSpaceAction hypothesis is needed: e.g. for a non-free action such as $\mathbb Z/2$ acting on a point (which violates condition 2), $\pi_1(Y/G)/H$ is trivial but $G$ is not, so the statement would be false without it.
• Universe-polymorphic in G, Y independently.