In mathematics, a class formation is a topological group acting on a module satisfying certain conditions.
If E is a subgroup of G, then AE is defined to be the elements of A fixed by E. We write for the Tate cohomology group Hn(E/F, AF) whenever E/F is a normal layer.
It is usually proved using properties of the Herbrand quotient, in the more precise form It is fairly straightforward to prove, because the Herbrand quotient is easy to work out, as it is multiplicative on short exact sequences, and is 1 for finite modules.
By studying the Dedekind zeta function of K one shows that the degree 1 primes of K have Dirichlet density given by the order of the pole at s=1, which is 1 (When K is the rationals, this is essentially Euler's proof that there are infinitely many primes using the pole at s=1 of the Riemann zeta function.)
(In fact, equality holds for all normal layers, but this takes more work; see the next section.)
The proof for arbitrary extensions uses a homomorphism from the group G onto the profinite completion of the integers with kernel G∞, or in other words a compatible sequence of homomorphisms of G onto the cyclic groups of order n for all n, with kernels Gn.
As these extensions are given explicitly one can check that they have the property that H2(G/Gn) is cyclic of order n, with a canonical generator.
This shows that the second cohomology group H2(E/F) of any layer is cyclic of order |E/F|, which completes the verification of the axioms of a class formation.
In other words, we have an explicit description of the abelianization of the Galois group E/F in terms of AE.
The main remaining theorem of class field theory is the Takagi existence theorem, which states that every finite index closed subgroup of the idele class group is the group of norms corresponding to some abelian extension.
For local class field theory, it is also possible to construct abelian extensions more explicitly using Lubin–Tate formal group laws.
For global fields, the abelian extensions can be constructed explicitly in some cases: for example, the abelian extensions of the rationals can be constructed using roots of unity, and the abelian extensions of quadratic imaginary fields can be constructed using elliptic functions, but finding an analog of this for arbitrary global fields is an unsolved problem.
If E/F is a normal layer, then the Weil group U of E/F is the extension corresponding to the fundamental class uE/F in H2(E/F, AF).