Fix a field and let be a separable closure. Let . Today we prove the strongest structure theorem so far: The category of separable -algebras is anti-equivalent to the category of finite -sets (where the action is continuous). Recall that one way to phrase the action being continuous on is to say that is a union of sets on which the action factors through some finite quotient .

To show the theorem let’s construct our functor -Set (I made this notation up just now, so it isn’t standard). Define . Recall from last time that our separable -algebra must have the form where are finite separable field extensions. Thus a map kills all factors except one which lands inside a finite separable extension of .

The -action on is the one given by acting on . More specifically, given and , we need to define a new -algebra map , but we do this by mapping . If you try this trick in other situations, be careful. It works here because any element fixes and hence preserves the -algebra structure. Suppose , then the action factors through and hence the action is continuous.

Now we get the rest of being a contravariant functor for free because we defined it to be , so any gives us by composing . Of course a morphism in must respect the -action, but this is true by construction.

We must check that we have a bijection on Hom sets. Suppose we have a -homomorphism , i.e. . We’ll show that and . Thus applying to both sides gives us a map . Keeping track of the action we can take the invariants to get . Thus from knowledge of we can completely recover our map which shows the functor is fully faithful.

The above argument requires us to keep careful track of the action to know it works. Let’s check the isomorphism . The map is given by where the map (evaluation on the first factor followed by multiplication). The action on the left is and the action on the right is conjugation . Let’s check equivariance of . Consider

. Thus the isomorphism preserves the -action and we see the previous paragraph goes through.

Lastly we need to know the functor is essentially surjective. Let be an arbitrary -set. Since is a disjoint union of its orbits and if , then , we may assume without loss of generality assume the action of is transitive. We know that factors through for some finite extension . Let so that the orbit of is all of . The stabilizer of is some subgroup of and so we can define the fixed field . Now we’re done, because and the -action is transitive by Galois theory. Thus the map determined by is a -isomorphism.

Our functor is fully faithful and essentially surjective and hence is an anti-equivalence of categories.