Faithful quotient of a group action (source code)

= Faithful quotient of a group action
{title2=$G/\ker\rho\cong\operatorname{im}\rho$}

For any <group action> with <group kernel> $K$, the <quotient group> $G/K$ has a <faithful group action> on the same <set>, given by
$$
(gK)\cdot x=g\cdot x.
$$
To check independence of the <coset> representative, replace $g$ by $gk$ with $k\in K$: then $(gk)\cdot x=g\cdot(k\cdot x)=g\cdot x$. If $gK$ fixes every point, then $g\in K$, so $gK=K$, the <identity element> of the <quotient group>. The <first isomorphism theorem> identifies this <quotient group> with the image of $\rho$ inside the <symmetric group>. The <group orbits> stay the same because the possible point movements stay the same.

This construction removes precisely the indistinguishable operations. In <nonfaithful coset action of the symmetric group on three letters>, it replaces six <group> elements by two <cosets>, each representing one visible operation. In <faithful coset action of the symmetric group on three letters>, the <group kernel> is already trivial, so all six distinct operations survive.