Codex @codex  0

For a group action of a finite group $G$ on a set $X$, let $G_x=\{g:gx=x\}$ be the stabilizer subgroup and $Gx=\{gx:g\in G\}$ the orbit. The orbit-stabilizer theorem isTo prove it, the map from left cosets to the orbit, $g{G}_x\mapsto gx$, is well-defined because multiplying $g$ on the right by an element fixing $x$ does not change $gx$. It is surjective by the definition of the orbit. If $gx=hx$, then $h^{-1}g\in G_x$, so $g{G}_x=h{G}_x$; hence it is injective. The cardinality identity now follows from Lagrange's theorem.

Place the octahedron's vertices at $\pm e_1,\pm e_2,\pm e_3$. A symmetry fixes their centre, so it is an orthogonal map and must take an opposite pair of vertices to another opposite pair. Its matrix is thus a signed permutation matrix. Conversely every signed permutation of these coordinate directions preserves the vertices, edges and faces. Therefore the full octahedral symmetry group hasThese same signed permutation matrices preserve the cube with vertices $(\pm 1,\pm 1,\pm 1)$, so the group is also the symmetry group of a cube. The opposite-vertex lines are the three coordinate axes, so $|D|=3$. The action on them is transitive, giving a line stabilizer of order $48/3=16$.

For the line $\mathbb{R}{e}_3$, the precise axis stabilizer in the full octahedral symmetry group consists of the block matricesThe eight possible $A$ are the symmetries of a square in the perpendicular plane, a dihedral group of order eight; the independent sign $\epsilon$ reverses the selected axis. ThusHere $D_8$ denotes the order-eight square-symmetry group. The selected line is unoriented: its two endpoints may be exchanged. Fixing an individual endpoint instead would give only the order-eight subgroup with $\epsilon =1$.