| Version 13 |
Version 12 |
| Given a group $G$ \PMlinkname{acting}{GroupAction} on a set $X$, define $Gx$ to be the orbit of $x$ and $G_x$ to be the stabilizer of $x$. |
Given a group $G$ \PMlinkname{acting}{GroupAction} on a set $X$, define $Gx$ to be the orbit of $x$ and $G_x$ to be the stabilizer of $x$. |
| For each $x\in X$, let ${\cal L}_x$ be the set of left cosets of $G_x$, |
For each $x\in X$, let ${\cal L}_x$ be the set of left cosets of $G_x$, |
| then the function $f\colon Gx\to{\cal L}_x$ |
then the function $f\colon Gx\to{\cal L}_x$ |
| defined by $f(gx)=gG_x$ for each $g\in G$ is a bijection. |
defined by $f(gx)=gG_x$ for each $g\in G$ is a bijection. |
| Therefore |
Therefore |
| $$|Gx| = [G:G_x]$$ |
$$|Gx| = [G:G_x]$$ |
| for all $x\in X$. |
for all $x\in X$. |
| It follows also that |
It follows also that |
| $$|Gx|\cdot|G_x| = |G|$$ |
$$|Gx|\cdot|G_x| = |G|$$ |
| for all $x\in X$. |
for all $x\in X$. |
|
|
| {\bf Proof}:\\ |
|
| The function $f$ is clearly surjective. |
|
| It is injective because if $gG_x = g'G_x$ then $g = g'h$ for some $h \in G_x$. |
|
| Therefore $g\cdot x = (g'h)\cdot x= g'\cdot(h\cdot x) = g'\cdot x$. |
|
