Reciprocity for abelian layers and the lattice of norm subgroups

Let cf be a class formation on a formation F over a profinite group G, with ground level A^G. An open normal subgroup V of G cuts out the layer V ◁ G, whose norm subgroup F.normSubgroup V ⊆ A^G is read in the common ground level. When the layer is abelian, that is when G ⧸ V is commutative, the Artin map of the layer needs no abelianization: it is a surjection A^G → G ⧸ V onto the Galois group of the layer itself (ClassFormation.abelianArtinMap), with kernel the norm subgroup (ClassFormation.ker_abelianArtinMap). In particular the norm subgroup has index the degree [G : V] (ClassFormation.index_normSubgroup).

For abelian U ≤ V the Artin symbol in G ⧸ V is the image of the one in G ⧸ U (ClassFormation.galHom_abelianArtinMap). So, inside one finite abelian quotient G ⧸ U, the norm subgroups of all layers between U and G are the preimages of the corresponding subgroups of G ⧸ U (ClassFormation.toAddSubgroup_normSubgroup_eq_comap). This turns the lattice of norm subgroups into the lattice of subgroups of a finite abelian group:

• the compositum of two abelian layers has the intersection of their norm subgroups as its norm subgroup (ClassFormation.normSubgroup_inf_of_isAbelian);
• the intersection of any two layers has the sum of their norm subgroups as its norm subgroup (ClassFormation.normSubgroup_sup; by norm limitation no abelianity is needed);
• a layer lies below an abelian layer exactly when its norm subgroup lies in that of the abelian layer (ClassFormation.normSubgroup_le_iff_of_isAbelian), so an abelian layer is determined by its norm subgroup (ClassFormation.eq_of_normSubgroup_eq_of_isAbelian);
• upward closure: a subgroup of A^G containing the norm subgroup of a layer is the norm subgroup of an abelian layer (ClassFormation.exists_abelianLayer_normSubgroup_eq_of_le), and so is one containing the norm group of any open subgroup, normal or not (ClassFormation.exists_abelianLayer_normSubgroup_eq_of_range_levelNorm_le);
• descent along a finite extension: a subgroup of A^G whose preimage under the norm from an open subgroup U contains the norm subgroup of a layer over U is the norm subgroup of an abelian layer of G (ClassFormation.exists_abelianLayer_normSubgroup_eq_of_normSubgroup_le_comap).

None of these is an existence theorem: the class-formation axioms do not say which subgroups of A^G contain a norm subgroup. The local and global class-field correspondences combine these statements with the arithmetic existence theorems of their own settings.

Main definitions

• TauCeti.ClassFieldTheory.ClassFormation.abelianArtinMap: the Artin map A^G → G ⧸ V of an abelian layer, written additively.

Main results

• TauCeti.ClassFieldTheory.ClassFormation.ker_abelianArtinMap and TauCeti.ClassFieldTheory.ClassFormation.surjective_abelianArtinMap: reciprocity for an abelian layer, A^G / N(V) ≃ G ⧸ V.
• TauCeti.ClassFieldTheory.ClassFormation.index_normSubgroup: [A^G : N(V)] = [G : V] for an abelian layer.
• TauCeti.ClassFieldTheory.ClassFormation.normSubgroup_inf_of_isAbelian and TauCeti.ClassFieldTheory.ClassFormation.normSubgroup_sup: the lattice laws.
• TauCeti.ClassFieldTheory.ClassFormation.normSubgroup_le_iff_of_isAbelian: layers are ordered against an abelian layer by their norm subgroups.
• TauCeti.ClassFieldTheory.ClassFormation.exists_abelianLayer_normSubgroup_eq_of_le: upward closure of norm subgroups.
• ClassFormation.exists_abelianLayer_normSubgroup_eq_of_range_levelNorm_le: upward closure from the norm group of an open subgroup.
• ClassFormation.exists_abelianLayer_normSubgroup_eq_of_normSubgroup_le_comap: descent of norm subgroups along a finite extension.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §6.
• J. S. Milne, Class Field Theory, Chapter VII, Lemmas 9.1 and 9.4.
• J.-P. Serre, Local Fields, Chapter XIV, §6.

Reciprocity onto the Galois group of an abelian layer

noncomputable def TauCeti.ClassFieldTheory.ClassFormation.abelianArtinMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) : ↥(F.level ⊤) →+ Additive (NormalLayer.ofOpenNormal V).Gal

The Artin map of an abelian layer V ◁ G, read on the ground level A^G and with values in the Galois group G ⧸ V of the layer itself, written additively. Since the layer is abelian, abelianizationGalEquiv removes the abelianization from the target of ClassFormation.artinMap (ofMul_of_abelianArtinMap).

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.ofMul_of_abelianArtinMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) (a : ↥(F.level ⊤)) : Additive.ofMul (Abelianization.of (Additive.toMul ((cf.abelianArtinMap hV) a))) = (cf.artinMap (NormalLayer.ofOpenNormal V)) ((NormalLayer.groundEquivOfOpenNormal F V) a)

The abelianization class of the Artin symbol abelianArtinMap is the Artin map of the layer.

theorem TauCeti.ClassFieldTheory.ClassFormation.abelianArtinMap_eq_zero_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) {a : ↥(F.level ⊤)} : (cf.abelianArtinMap hV) a = 0 ↔ a ∈ F.normSubgroup V

The Artin symbol of an abelian layer vanishes exactly on the norm subgroup.

theorem TauCeti.ClassFieldTheory.ClassFormation.ker_abelianArtinMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) : (cf.abelianArtinMap hV).ker = (F.normSubgroup V).toAddSubgroup

The kernel of the Artin map of an abelian layer is its norm subgroup.

theorem TauCeti.ClassFieldTheory.ClassFormation.surjective_abelianArtinMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) : Function.Surjective ⇑(cf.abelianArtinMap hV)

The Artin map of an abelian layer is surjective.

theorem TauCeti.ClassFieldTheory.ClassFormation.index_normSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) : (F.normSubgroup V).toAddSubgroup.index = (NormalLayer.ofOpenNormal V).degree

The norm index of an abelian layer is its degree: [A^G : N(V)] = [G : V].

Norm subgroups through a common abelian refinement

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.galHom_abelianArtinMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {U V : OpenNormalSubgroup G} (hU : U.IsAbelianClassFieldLayer) (h : U ≤ V) (a : ↥(F.level ⊤)) : ⋯.galHom (Additive.toMul ((cf.abelianArtinMap hU) a)) = Additive.toMul ((cf.abelianArtinMap ⋯) a)

The Artin symbol of a quotient layer. For abelian U ≤ V, the Artin symbol of a ∈ A^G in G ⧸ V is the image of its Artin symbol in G ⧸ U under the quotient map.

theorem TauCeti.ClassFieldTheory.ClassFormation.toAddSubgroup_normSubgroup_eq_comap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {U V : OpenNormalSubgroup G} (hU : U.IsAbelianClassFieldLayer) (h : U ≤ V) : (F.normSubgroup V).toAddSubgroup = AddSubgroup.comap (cf.abelianArtinMap hU) (Subgroup.toAddSubgroup ⋯.galHom.ker)

The norm subgroup of a quotient layer, read in a refinement. For abelian U ≤ V, an element of A^G is a norm from the layer of V exactly when its Artin symbol in G ⧸ U lies in the kernel of the quotient map G ⧸ U → G ⧸ V.

Composita and intersections

theorem TauCeti.ClassFieldTheory.ClassFormation.normSubgroup_inf_of_isAbelian {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V W : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) (hW : W.IsAbelianClassFieldLayer) : F.normSubgroup (V ⊓ W) = F.normSubgroup V ⊓ F.normSubgroup W

Composita. For abelian layers V and W, the norm subgroup of their compositum, cut out by V ⊓ W, is the intersection of the two norm subgroups. Abelianity is needed: by norm limitation the left side only sees the maximal abelian sublayer of V ⊓ W, which can be larger than the compositum of the maximal abelian sublayers of V and W.

theorem TauCeti.ClassFieldTheory.ClassFormation.normSubgroup_sup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (V W : OpenNormalSubgroup G) : F.normSubgroup (V ⊔ W) = F.normSubgroup V ⊔ F.normSubgroup W

Intersections. The norm subgroup of the intersection of the layers of V and W, which is cut out by V ⊔ W, is the sum of the two norm subgroups. No abelianity is needed: by norm limitation every norm subgroup is that of its maximal abelian sublayer, and the maximal abelian sublayer of V ⊔ W is the join of those of V and W.

Abelian layers are determined by their norm subgroups

theorem TauCeti.ClassFieldTheory.ClassFormation.normSubgroup_le_iff_of_isAbelian {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V W : OpenNormalSubgroup G} (hW : W.IsAbelianClassFieldLayer) : F.normSubgroup V ≤ F.normSubgroup W ↔ V ≤ W

Abelian layers are ordered by their norm subgroups. For an abelian layer W and any layer V, the norm subgroup of V lies in that of W exactly when V ≤ W; on the extensions they cut out, the inclusion is reversed. No abelianity of V is needed: by norm limitation V has the norm subgroup of its maximal abelian sublayer.

theorem TauCeti.ClassFieldTheory.ClassFormation.eq_of_normSubgroup_eq_of_isAbelian {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V W : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) (hW : W.IsAbelianClassFieldLayer) (h : F.normSubgroup V = F.normSubgroup W) : V = W

An abelian layer is determined by its norm subgroup. The abelianity hypotheses are essential: by norm limitation every layer has the norm subgroup of its maximal abelian sublayer.

Upward closure

theorem TauCeti.ClassFieldTheory.ClassFormation.exists_abelianLayer_normSubgroup_eq_of_le {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {V : OpenNormalSubgroup G} {N : Submodule ℤ ↥(F.level ⊤)} (h : F.normSubgroup V ≤ N) : ∃ (W : OpenNormalSubgroup G), W.IsAbelianClassFieldLayer ∧ V ≤ W ∧ F.normSubgroup W = N

Upward closure of norm subgroups. In a class formation, a subgroup N of A^G containing the norm subgroup of the layer V ◁ G is the norm subgroup of an abelian layer W ≥ V. By norm limitation V may be replaced by its maximal abelian sublayer U, whose Artin map A^G → G ⧸ U is surjective with kernel the norm subgroup; W is the preimage in G of the image of N. This is not an existence theorem: it only applies to subgroups already known to contain a norm subgroup.

theorem TauCeti.ClassFieldTheory.ClassFormation.exists_abelianLayer_normSubgroup_eq_of_range_levelNorm_le {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {W : OpenSubgroup G} {N : Submodule ℤ ↥(F.level ⊤)} (h : (F.levelNorm ⋯).range ≤ N.toAddSubgroup) : ∃ (V : OpenNormalSubgroup G), V.IsAbelianClassFieldLayer ∧ F.normSubgroup V = N

Upward closure from an open subgroup. In a class formation, a subgroup N of A^G containing the image of the norm N_{G/W} : A^W → A^G from an open subgroup W, normal or not, is the norm subgroup of an abelian layer. In field notation: a subgroup containing the norm group N_{E/K}(A_E) of a finite, not necessarily Galois, extension E/K is a norm subgroup. The open normal subgroups below W, which cut out the Galois extensions containing E, have smaller norm subgroups (Formation.normSubgroup_le_range_levelNorm), so upward closure applies.

theorem TauCeti.ClassFieldTheory.ClassFormation.exists_abelianLayer_normSubgroup_eq_of_normSubgroup_le_comap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) {N : Submodule ℤ ↥(F.level ⊤)} (h : (L.normSubgroup F).toAddSubgroup ≤ AddSubgroup.comap (F.levelNorm ⋯) N.toAddSubgroup) : ∃ (V : OpenNormalSubgroup G), V.IsAbelianClassFieldLayer ∧ F.normSubgroup V = N

Descent of norm subgroups along a finite extension. Let L be a layer W ◁ U, cutting out a Galois extension M/E above a finite extension E/K. In a class formation, if the preimage of a subgroup N ⊆ A^G under the norm N_{G/U} : A^U → A^G contains the norm subgroup N_{U/W}(A^W) of L, then N is the norm subgroup of an abelian layer of G. In field notation: if N_{E/K}⁻¹(N) contains N_{M/E}(A_M), then N contains N_{M/K}(A_M) by transitivity of the norm, so it is a norm subgroup by exists_abelianLayer_normSubgroup_eq_of_range_levelNorm_le. This is the step of the proof of the existence theorem that passes from K to K(ζ_p) (Milne VII, Lemma 9.4).