The idelic consequence of Furtwängler's theorem

Let L/F be a finite Galois extension of number fields inside a separable closure, and let E be its maximal abelian subextension. Every idele class of F, extended to E, is a norm of an idele class of L (ideleClassExtension_mem_range_ideleClassNormMap_commutator). Equivalently, the extension map C_F → C_E becomes trivial modulo N_{L/E}(C_L).

The fields are identified by the finite layers of the global formation: if Lay represents L/F, then the ground field of Lay.subgroupLayer (commutator Lay.Gal) is E. No abelianity of L/F or unramifiedness is needed. Inclusion of ground levels is extension of idele classes, and the abstract principal ideal theorem for globalClassFormation makes its image a norm.

This is the norm-theoretic input to ideal principalization: applying it to the Hilbert class field tower additionally requires identifying its maximal abelian subextension and identifying the norm subgroup at its upper step with the trivial-modulus ray subgroup. The result here does not assert that ideals principalize in the maximal abelian subextension of an arbitrary L/F.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIII.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §7 (the principal ideal theorem).

theorem TauCeti.ClassFieldTheory.ideleClassExtension_mem_range_ideleClassNormMap_commutator {K : Type} [Field K] [NumberField K] {F E L : IntermediateField K (SeparableClosure K)} [NumberField ↥F] [NumberField ↥E] [NumberField ↥L] [Algebra ↥F ↥E] [IsScalarTower (↥F) (↥E) (SeparableClosure K)] [Algebra ↥E ↥L] [IsScalarTower (↥E) (↥L) (SeparableClosure K)] (Lay : NormalLayer (AbsoluteGaloisGroup K)) (hF : IntermediateField.fixedField ↑Lay.ground = F) (hE : IntermediateField.fixedField ↑(Lay.subgroupLayer (commutator Lay.Gal)).ground = E) (hL : IntermediateField.fixedField ↑Lay.top = L) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥F) ↥F) : (GlobalNumberFields.ideleClassExtension ↥F ↥E) c ∈ (↑(GlobalNumberFields.ideleClassNormMap ↥E ↥L)).range

The idelic consequence of Furtwängler's theorem. If Lay represents L/F and E is its maximal abelian subextension, every idele class of F, extended to E, is a norm from L. The field E is pinned as the fixed field of the preimage of the commutator subgroup of the finite Galois group; no norm or principalization hypothesis is assumed.

theorem TauCeti.ClassFieldTheory.ideleClassExtension_mem_range_ideleClassNormMap_commutator_ofOpenNormal {K : Type} [Field K] [NumberField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) {E L : IntermediateField K (SeparableClosure K)} [NumberField ↥E] [NumberField ↥L] [Algebra ↥E ↥L] [IsScalarTower (↥E) (↥L) (SeparableClosure K)] (hE : IntermediateField.fixedField ↑((NormalLayer.ofOpenNormal V).subgroupLayer (commutator (NormalLayer.ofOpenNormal V).Gal)).ground = E) (hL : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal V).top = L) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (GlobalNumberFields.ideleClassExtension K ↥E) c ∈ (↑(GlobalNumberFields.ideleClassNormMap ↥E ↥L)).range

Idele classes of the base field become norms over the maximal abelian subextension. For the finite Galois extension cut out by V, with top field L and maximal abelian subextension E, the image of C_K → C_E lies in N_{L/E}(C_L).