The following exposition is an attempt to extract the essence of the argument why localic subgroups of localic groups are closed. It avoids all the diagrams and technical machinery, which, though necessary for a proper proof, might well prove tedious to the reader who is not an expert in the field but who nonetheless has background knowledge of topology or logic.
To recapitulate: a frame is a complete lattice in which finite infima distribute over suprema; a locale X is determined by a frame O(X); a map of locales f : X -> Y is determined by a homomorphism of frames (preserves suprema and finite infima) O(Y) -> O(X). By this means traditional topology, based on the abstraction of points , is replaced by locale theory which is based on the abstraction of (a frame of) experiments .
The category of locales fully includes the category of sober topological spaces and continuous functions if we identify a space with the locale whose frame is the lattice of the space's open subsets. A sublocale Y of a locale X is determined by a quotient frame of O(X), which in turn is determined by a congruence on O(X); that is to say an equivalence relation on O(X) that respects the operations of supremum and of finite infimum. The standard notions of topology can be re-expressed for locales, so that we can talk of the closure of a sublocale, dense sublocales, the interior of a sublocale etc.
Complete Boolean algebras are automatically frames. Every frame has a special quotient, its booleanization . This is the complete Boolean algebra obtained by identifying each element u of the frame with not(not(u)) where not(x) is the supremum of all the elements of the frame whose infimum with x is 0, the minimum element. If the frame is nontrivial, its Booleanization is nontrivial. So for any locale X we have a special sublocale #X of X, where O(#X) is the Booleanization of O(X). The following facts about dense sublocales are straightforward to verify and are crucial to the argument:
As a consequence we deduce that any intersection of dense sublocales is a dense sublocale. This result is interesting because the analogue for topological spaces is false (think of the rationals and the irrationals, both dense subsets of the real line). On the other hand its analogue in algebraic geometry does hold and has important consequences.
By a localic group we mean a group in the category of locales. Every locally compact Hausdorff topological group yields an example. If G is a localic group and we have two sublocales A and B of G then we may define a sublocale AB by taking the image of the map AxB -> G got by composing the inclusion map AxB -> GxG with the group composition GxG -> G. Similarly we may define the inverse of A by using the inverse operation G -> G. Of course these operations coincide with what is usually defined in terms of points in the context of topological groups, but we have to remember that locales are not defined by their points but by their frames. Every localic group G does have a special point, its identity element e.
Proposition 1: Let A and B be sublocales of a localic group G. If A has nonempty intersection with B, then e belongs to A times the inverse of B.
It is easy to understand why in terms of points. If x belongs to both A and B then e = x times inverse of x belongs to A times inverse of B. However there is a point-free proof of this result.
Proposition 2: Let S be a dense sublocale of a localic group G. Then S times the inverse of S is the whole of G.
In terms of points, if we take A to be the inverse of g times S and B = S for some generic point g of G then A and B, being dense, have nonempty intersection. So by proposition 1 we have that e belongs to (inverse of g) times S times (inverse of S) which implies that g belongs to S times inverse of S. Again, there is a point-free proof of this result.
The Closed Subgroup Theorem: Any localic subgroup of a localic group is closed.
Let H be a localic subgroup of a localic group G. It is straightforward to show that the closure of H in G is again a localic subgroup, so we might as well replace G by this closure, or equivalently, assume that H is dense in G. Since H equals its own inverse and HH = H proposition 2 shows that H = G.
A Galois group is really a localic group, of course. So intermediate extensions of fields in a separable algebraic extension of fields correspond to localic subgroups (tout court) of the Galois group of the extension.