Proof of The Orbit–Stabilizer Theorem

Routine facts about nonempty and disjoint classes are used without comment (Toolkit for AL1).

We first note that acting by $g^{-1}$ undoes acting by $g$: for $g\in G$ and $y,z\in X$,

$$z=g\cdot y\iff y=g^{-1}\cdot z.\tag{E}$$

This follows from the two identities of Group Actions (i) together with $g^{-1}g=e=gg^{-1}$ (Uniqueness of the Identity Element and of Inverses in a Group (ii)): if $z=g\cdot y$, then $g^{-1}\cdot z=(g^{-1}g)\cdot y=e\cdot y=y$, and if $y=g^{-1}\cdot z$, then $g\cdot y=(gg^{-1})\cdot z=z$.

For (i), $e\in G_{x}$ by Group Actions (i) and Orbits and Stabilizers (ii), so $G_{x}$ is nonempty. If $g,h\in G_{x}$, then $h^{-1}\cdot x=x$ by (E) applied to $h$ and $y=z=x$, and so

$$(gh^{-1})\cdot x=g\cdot(h^{-1}\cdot x)=g\cdot x=x.$$

Hence $G_{x}$ is a subgroup of $G$ by Subgroup Criterion and Basic Examples (i).

For (ii), (iii) and (iv), consider the relation $R=\{(y,z)\in X\times X:z\in Gy\}$. It is an equivalence relation on $X$: it is reflexive because $y=e\cdot y$, symmetric by (E), and transitive by the second identity of Group Actions (i). By Orbits and Stabilizers (i), the equivalence class of $y$ under $R$ (The Equivalence Class of an Element under an Equivalence Relation (i)) is the orbit $Gy$. The three assertions are therefore Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection (iv), Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection (i) and Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection (ii).

For (v), let $g,h\in G$. Using (E) and Group Actions (i), and then Left Cosets Partition a Group and All Have the Same Cardinality (ii),

$$g\cdot x=h\cdot x\iff(g^{-1}h)\cdot x=x\iff g^{-1}h\in G_{x}\iff gG_{x}=hG_{x}.$$

Every element of $G/G_{x}$ is a coset $gG_{x}$ (Cosets and the Index of a Subgroup (iii)). Reading this chain from right to left, the relation $\{(gG_{x},g\cdot x):g\in G\}$ is single-valued; its values $g\cdot x$ lie in $Gx$ (Orbits and Stabilizers (i)), so it is a function $\varphi$ from $G/G_{x}$ to $Gx$ (Functions, Values of a Function, and Functions from One Class to Another (iii)) with $\varphi(gG_{x})=g\cdot x$ for every $g\in G$. Any other function with these values agrees with $\varphi$ at every element of $G/G_{x}$, each element being some $gG_{x}$, and so equals $\varphi$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i). Reading the chain from left to right, $\varphi$ is injective (Injective, Surjective and Bijective Functions between Classes (i)), and it is surjective (Injective, Surjective and Bijective Functions between Classes (ii)) because every element of $Gx$ is some $g\cdot x$ (Orbits and Stabilizers (i)). So $\varphi$ is a bijection (Injective, Surjective and Bijective Functions between Classes (iii)).

For (vi), let $G$ be finite. Since $G_{x}$ is a subgroup by (i), Lagrange's Theorem (i) shows that $G/G_{x}$ is finite and

$$|G|=[G:G_{x}]\cdot|G_{x}|.$$

As $\varphi$ is a bijection from $G/G_{x}$ onto $Gx$ by (v), the orbit $Gx$ is finite with $\#(Gx)=\#(G/G_{x})=[G:G_{x}]$, by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vi), Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products (iii) and Cosets and the Index of a Subgroup (iv). Hence $|G|=\#(Gx)\cdot|G_{x}|$, and $\#(Gx)\mid|G|$, taking $k=|G_{x}|$ in Divisibility of Integers (i).