[proofplan]
We split the argument into two parts. For the forward direction, we first verify that the map $\Phi: G/H \to X$ defined by $gH \mapsto g \cdot x_0$ is well-defined (independent of coset representative), then prove it is injective, surjective, and $G$-equivariant. For the converse, we directly verify that the left multiplication action of $G$ on $G/H$ is transitive and compute the stabiliser of the identity coset $eH$.
[/proofplan]
[step:Verify that $\Phi$ is well-defined]
Suppose $gH = g'H$, so that $g' = gh$ for some $h \in H$. Then
\begin{align*}
\Phi(g'H) = g' \cdot x_0 = (gh) \cdot x_0 = g \cdot (h \cdot x_0) = g \cdot x_0 = \Phi(gH),
\end{align*}
where the third equality uses the action axiom $(gh) \cdot x_0 = g \cdot (h \cdot x_0)$, and the fourth uses $h \in H = G_{x_0}$, so $h \cdot x_0 = x_0$. Hence $\Phi$ does not depend on the choice of coset representative.
[guided]
We need to check that $\Phi$ gives the same output regardless of which representative we pick from the coset $gH$. Why might it fail? If $g'H = gH$, then $g' = gh$ for some $h \in H$. The map sends $g'H$ to $g' \cdot x_0 = (gh) \cdot x_0$. By the action axiom (compatibility of the group operation with the action), $(gh) \cdot x_0 = g \cdot (h \cdot x_0)$. Now the key point: $h \in H = G_{x_0}$ means precisely that $h \cdot x_0 = x_0$. So
\begin{align*}
\Phi(g'H) = g' \cdot x_0 = (gh) \cdot x_0 = g \cdot (h \cdot x_0) = g \cdot x_0 = \Phi(gH).
\end{align*}
This is the reason the stabiliser appears in the construction: we quotient by exactly the subgroup that fixes $x_0$, which is precisely what makes the map well-defined.
[/guided]
[/step]
[step:Prove that $\Phi$ is injective]
Suppose $\Phi(gH) = \Phi(g'H)$, i.e., $g \cdot x_0 = g' \cdot x_0$. Applying $g'^{-1}$ to both sides via the group action gives
\begin{align*}
(g'^{-1}g) \cdot x_0 = g'^{-1} \cdot (g \cdot x_0) = g'^{-1} \cdot (g' \cdot x_0) = (g'^{-1}g') \cdot x_0 = e \cdot x_0 = x_0.
\end{align*}
Hence $g'^{-1}g \in G_{x_0} = H$, so $gH = g'H$. Therefore $\Phi$ is injective.
[guided]
The question is: can two distinct cosets map to the same element of $X$? Suppose $\Phi(gH) = \Phi(g'H)$, meaning $g \cdot x_0 = g' \cdot x_0$. To show $gH = g'H$, it suffices to show $g'^{-1}g \in H$. We compute:
\begin{align*}
(g'^{-1}g) \cdot x_0 = g'^{-1} \cdot (g \cdot x_0) = g'^{-1} \cdot (g' \cdot x_0) = (g'^{-1}g') \cdot x_0 = e \cdot x_0 = x_0,
\end{align*}
where each step uses the action axiom $(ab) \cdot x = a \cdot (b \cdot x)$ and the identity axiom $e \cdot x = x$. Since $(g'^{-1}g) \cdot x_0 = x_0$, we have $g'^{-1}g \in G_{x_0} = H$, which gives $gH = g'H$.
Note the interplay: the stabiliser $H$ is exactly the "kernel" of $\Phi$ in the sense that $gH = g'H$ iff $g'^{-1}g$ fixes $x_0$. This is analogous to the First Isomorphism Theorem for groups, where the kernel of a homomorphism determines injectivity of the induced map on the quotient.
[/guided]
[/step]
[step:Prove that $\Phi$ is surjective using transitivity]
Let $x \in X$. Since the action $G \curvearrowright X$ is transitive, there exists $g \in G$ with $g \cdot x_0 = x$. Then $\Phi(gH) = g \cdot x_0 = x$, so $\Phi$ is surjective.
[/step]
[step:Verify that $\Phi$ is $G$-equivariant]
Let $g' \in G$ and $gH \in G/H$. The group $G$ acts on $G/H$ by left multiplication: $g' \cdot (gH) = (g'g)H$. We check:
\begin{align*}
\Phi(g' \cdot (gH)) = \Phi((g'g)H) = (g'g) \cdot x_0 = g' \cdot (g \cdot x_0) = g' \cdot \Phi(gH).
\end{align*}
Hence $\Phi$ intertwines the $G$-action on $G/H$ with the $G$-action on $X$, i.e., $\Phi$ is a $G$-equivariant bijection and therefore an isomorphism of $G$-sets.
[/step]
[step:Prove the converse: the coset action on $G/H$ is transitive with stabiliser $H$]
Let $H \le G$. The group $G$ acts on the set $G/H = \{gH : g \in G\}$ by left multiplication: $g' \cdot (gH) = (g'g)H$.
**Transitivity.** Let $gH \in G/H$ be any coset. Then $g \cdot (eH) = (ge)H = gH$, so every coset is in the orbit of $eH$. Hence the action is transitive.
**Stabiliser of $eH$.** We compute
\begin{align*}
G_{eH} = \{g \in G : g \cdot (eH) = eH\} = \{g \in G : gH = H\} = \{g \in G : g \in H\} = H,
\end{align*}
where $gH = H$ iff $g = ge \in H$. Therefore the stabiliser of the identity coset is precisely $H$.
[guided]
For the converse, we start with an abstract subgroup $H \le G$ and build a transitive $G$-set from it. Define the action $G \curvearrowright G/H$ by $g' \cdot (gH) = (g'g)H$.
We must first verify this action is well-defined, i.e., that the result does not depend on the choice of coset representative. Suppose $gH = g_1H$, so $g_1 = gh$ for some $h \in H$. Then $(g'g_1)H = (g'gh)H = (g'g)H$, since $h \in H$ means $ghH = gH$. The action axioms are immediate: $e \cdot (gH) = (eg)H = gH$, and $(g_1 g_2) \cdot (gH) = (g_1 g_2 g)H = g_1 \cdot ((g_2 g)H) = g_1 \cdot (g_2 \cdot (gH))$.
**Transitivity.** Given any coset $gH \in G/H$, the element $g \in G$ sends the identity coset to it: $g \cdot (eH) = (ge)H = gH$. So every coset lies in the orbit of $eH$, and the action is transitive.
**Stabiliser of $eH$.** An element $g \in G$ stabilises $eH$ iff $g \cdot (eH) = eH$, i.e., $gH = H$. Now $gH = H$ iff $g = ge \in H$ (a coset $gH$ equals $H$ precisely when the representative $g$ belongs to $H$). Therefore
\begin{align*}
G_{eH} = \{g \in G : gH = H\} = H.
\end{align*}
This shows that every subgroup $H \le G$ arises as the stabiliser of some transitive $G$-action, and the forward direction shows that every transitive action arises (up to isomorphism of $G$-sets) as a coset action. Together, the two directions establish a bijective correspondence between conjugacy classes of subgroups of $G$ and isomorphism classes of transitive $G$-sets: the basepoint $x_0$ determines $H = G_{x_0}$ up to conjugacy (changing the basepoint conjugates the stabiliser), and conversely $H$ determines $G/H$ up to $G$-equivariant bijection.
[/guided]
[/step]
