Why isn't the orbit-stabilizer theorem obvious?

The title of this post paraphrases the title of a great blog post by Timothy Gowers, where he argues that those who think that the fundamental theorem of arithmetic is obvious are almost certainly missing something.

I was reminded of this blog post while reading another blog post by the very same author on the orbit-stabilizer theorem of basic group theory.

This theorem has always seemed pretty obvious to me, but when I try to follow the several proofs of it that Gowers gives for it in this post I have such a hard time of it that I have to wonder if it is now I who has been taking for obvious what really isn't.

My thinking goes something like this: Let $G$ be a group that acts on a set $X$, let $x$ be an element of $X$, let $O_x$ be the orbit of $x$ and let $S_x$ be the stabilizer of $x$. (The last sentence is lifted verbatim from Gowers' post.) We want to show that $|G| = |O_x||S_x|$. Now, $S_x$ is (obviously) a subgroup of $G$, and the formula to be proved is just Lagrange's theorem applied to this subgroup. This is because two elements of $G$ send $x$ to the same element of $O_x$ if and only if they belong to the same coset of $S_x$, and therefore $|O_x| = [G:S_x]$. More formally, the map $gS_x \mapsto gx$ is injective, because

$$gx = hx \; \; \Rightarrow \; \; h^{-1}gx = x \; \; \Rightarrow \; \; h^{-1}g \in S_x \; \; \Rightarrow \; \; gS_x = hS_x,$$

or, taking the contrapositive,

$$gS_x \neq hS_x \; \; \Rightarrow \; \; gx \neq hx.$$

It is also surjective, since every $gx \in O_x$ is the image of $gS_x$ under this map.

It's a bit painful to see how much writing it takes to spell out a perception that in my mind is literally instantaneous. Even so, the reasoning above, as belabored as it is, is, IMO, more succinct and straightforward than Gowers'.

Am I missing something?

Are you missing some mathematical subtlety by thinking that the Orbit-Stabilizer Theorem is very easy to prove? No, I don't think so: your proof is correct. Moreover, I skimmed Gowers's blog post and I don't think he says or intends to say that OST is in some way deep or nonobvious. In fact I think the goal of the post is essentially the opposite: to convince a beginner in abstract algebra that OST is, if not completely obvious, then quite easy: easy enough for someone to fully understand and remember the proof for ever after.

Gowers gives several different proofs (or maybe more accurately, several different expositions of a proof) of OST. Some of them take only a few lines. The fact that his whole discussion is rather lengthy is because he is trying to teach the obviousness of OST to someone who is not very comfortable or familiar with algebraic arguments. That is, by the way, a truly high-level teaching maneuver: it would be so much easier just to write down a three line proof and leave the task of interpreting it to the student.

Here is one big difference between OST and FTA: the statement of FTA is incredibly easy and familiar, using only concepts that are truly well known to most educated people. Moreover, since most people learn about factoring numbers in school, the level of experience with the conclusion of FTA is essentially maximal. That's not true for OST: how much time passes between most students' learning the definition of a group action and learning the statement of OST: a week? Less? It's a much different situation: modern mathematics has to be taught carefully so as not to be a sequence of answers to questions that no one has thought (or been given the chance to think) to ask.

OST is one of those theorems for which finding the statement is much more of an achievement than finding the proof. Such theorems are not inherently less useful than "deeper" theorems.

Let me take things a step further: what you state (which is what Gowers states) as OST is not what I think of as OST but rather a corollary of it. What I think of OST is a slightly more complicated statement that has the proof built into it to a larger degree. Namely:

Orbit Stabilizer Theorem: Let $G$ be a group acting on a set $X$. For $x \in X$, let $H_x$ be the stabilizer of $x$. Then there is a well-defined $G$-set isomorphism $\Phi: G/H_x \stackrel{\sim}{\rightarrow} G x$, $gH_x \mapsto gx$.

Notice that if you combine this with Lagrange's Theorem -- for a subgroup $H$ of a group we have $(\# H)(\# G/H) = \# G$ -- then we get the earlier statement of OST. But because we've put more into the statement (my statement is more "categorified" than yours, but let's not get into that here), it really is obvious. Or more precisely it is as obvious as it could possibly be: you need to know the meanings of all the terms involved, which for a beginner at algebra is hard work (which I think is why Gowers did not choose to state OST this way). If you know all the lingo, here is the proof:

$\bullet$ $\Phi$ is well-defined: if $gH_x = g' H_x$, then $ g^{-1}g' \in H_x$, so $g x = g (g^{-1} g' x) = g' x$.

$\bullet$ $\Phi$ is surjective: yes, it is!

$\bullet$ $\Phi$ is injective: If $\Phi(g H_x) = \Phi(g' H_x)$ then $gx = g' x$ so $g^{-1} g' x = x$, so $g^{-1} g' \in H_x$, so $g H_x = g' H_x$.

$\bullet$ $\Phi$ is a $G$-map: if $g \in G$ and $z = g' H_x \in G/H_x$, then $g\Phi(z) = g\Phi(g'H_x) = g(g'x) = (gg')x = \Phi((gg') H_x) = \Phi(g(g'H_x)) = \Phi(gz)$.

Note that in the above, I didn't try to write things as briefly as possible. On the contrary, I gave every detail (perhaps even obnoxiously so, in the last line). Whether something is "obvious" should not (I think) be measured in how many lines it takes to express the formal verification that you have in your head, but in how long it takes you to find the formal verification.

I would say that the theorem is pretty obvious.

However, if you look at Gowers's post, he is trying to do a bit more than just prove the theorem:

• Firstly, he is not proceeding via quoting Lagrange's theorem, but is rather building the proof of this particular case of Lagrange's theorem into his argument.

• Secondly, he is furthermore interpeting the cosets of $S_x$ as being precisely the elements of $G$ that take $x$ to some other element $y$. In other words, he is exhibiting the bijection $G/S_x \cong X$, in a fairly concrete way.

• Finally, he is writing for beginners, and trying to put all his thoughts down on the page. The goal isn't to find the most succinct proof, but to try to make things clear to a motivated beginner who's willing to read the discussion carefully.

Conclusion: I don't think you're missing anything about the mathematics, but perhaps viewing Gowers's post through the prism of the most efficient proof is not quite the right thing to do.