Norm subgroups of abelian local layers

Let K be a nonarchimedean local field and V an open normal subgroup of its absolute Galois group G_K containing the closed commutator subgroup, so that V cuts out a finite abelian extension L/K with Galois group G_K ⧸ V. Local reciprocity for the local class formation then reads as an isomorphism onto the Galois group of the layer itself,

Kˣ / N_{L/K}(Lˣ) ≃ Gal(L/K),

with no abelianization left in the target (localAbelianGaloisEquiv). In particular the norm subgroup has index [L : K] (index_localNormSubgroup).

This is reciprocity for the abelian layers of a class formation (ClassFormation.abelianArtinMap), applied to the local class formation and read on Kˣ. The lattice laws of local norm subgroups are likewise those of the norm subgroups of a class formation (ClassFormation.normSubgroup_inf_of_isAbelian, ClassFormation.normSubgroup_sup), read on Kˣ through localGroundOrderIso: the compositum of two finite abelian extensions has the intersection of their norm subgroups as its norm subgroup (localNormSubgroup_inf_of_isAbelian), and the intersection of two finite Galois extensions has the product of their norm subgroups (localNormSubgroup_sup; by norm limitation this needs no abelianity).

Main definitions

• TauCeti.ClassFieldTheory.localAbelianGaloisEquiv: local reciprocity for an abelian layer, Kˣ / N_{L/K}(Lˣ) ≃* Gal(L/K).

Main results

• TauCeti.ClassFieldTheory.localAbelianGaloisEquiv_artinMap: localAbelianGaloisEquiv is the Artin map of the local class formation.
• TauCeti.ClassFieldTheory.index_localNormSubgroup: [Kˣ : N_{L/K}(Lˣ)] = [L : K] for an abelian layer.
• TauCeti.ClassFieldTheory.localNormSubgroup_inf_of_isAbelian: the norm subgroup of a compositum of finite abelian extensions is the intersection of their norm subgroups.
• TauCeti.ClassFieldTheory.localNormSubgroup_sup: the norm subgroup of an intersection of finite Galois extensions is the product of their norm subgroups.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §6.
• J.-P. Serre, Local Fields, Chapter XI, §3.

Reciprocity onto the Galois group of an abelian layer

noncomputable def TauCeti.ClassFieldTheory.localAbelianArtinHom (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) : Kˣ →* (NormalLayer.ofOpenNormal V).Gal

The Artin map of the local class formation on the layer V ◁ G_K, as a homomorphism from Kˣ: the Artin map ClassFormation.abelianArtinMap of the abelian layer, read on Kˣ through the identification of Kˣ with the ground level. For an abelian layer it is read in the Galois group itself rather than in its abelianization.

theorem TauCeti.ClassFieldTheory.localAbelianArtinHom_apply {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) (x : Kˣ) : (localAbelianArtinHom K hV) x = Additive.toMul (((localClassFormation K).abelianArtinMap hV) ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul x)))

localAbelianArtinHom is the Artin map of the abelian layer evaluated on x ∈ Kˣ, read in the ground level ((Kˢ)ˣ)^{G_K}.

@[simp]

theorem TauCeti.ClassFieldTheory.of_localAbelianArtinHom {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) (x : Kˣ) : Additive.ofMul (Abelianization.of ((localAbelianArtinHom K hV) x)) = ((localClassFormation K).artinMap (NormalLayer.ofOpenNormal V)) ((localGroundEquiv K V) (Additive.ofMul x))

The abelianization class of localAbelianArtinHom is the Artin map of the local class formation.

theorem TauCeti.ClassFieldTheory.ker_localAbelianArtinHom {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) : (localAbelianArtinHom K hV).ker = localNormSubgroup K V

The kernel of localAbelianArtinHom is the local norm subgroup.

theorem TauCeti.ClassFieldTheory.surjective_localAbelianArtinHom {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) : Function.Surjective ⇑(localAbelianArtinHom K hV)

localAbelianArtinHom is surjective.

noncomputable def TauCeti.ClassFieldTheory.localAbelianGaloisEquiv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) : Kˣ ⧸ localNormSubgroup K V ≃* (NormalLayer.ofOpenNormal V).Gal

Local reciprocity for an abelian layer, Kˣ / N_{L/K}(Lˣ) ≃* Gal(L/K). Its target is the Galois group G_K ⧸ V of the layer itself: since the layer is abelian, abelianizationGalEquiv removes the abelianization from the target of the Artin equivalence of the local class formation (localAbelianGaloisEquiv_artinMap).

@[simp]

theorem TauCeti.ClassFieldTheory.localAbelianGaloisEquiv_mk {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) (x : Kˣ) : (localAbelianGaloisEquiv K hV) ↑x = (localAbelianArtinHom K hV) x

localAbelianGaloisEquiv sends the class of x to its Artin symbol localAbelianArtinHom K hV x.

theorem TauCeti.ClassFieldTheory.localAbelianGaloisEquiv_artinMap {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) (x : Kˣ) : Additive.ofMul (Abelianization.of ((localAbelianGaloisEquiv K hV) ↑x)) = ((localClassFormation K).artinMap (NormalLayer.ofOpenNormal V)) ((localGroundEquiv K V) (Additive.ofMul x))

localAbelianGaloisEquiv is the Artin map of the local class formation: composed with Abelianization.of, which is injective because the layer is abelian, it is ClassFormation.artinMap.

theorem TauCeti.ClassFieldTheory.index_localNormSubgroup {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) : (localNormSubgroup K V).index = (NormalLayer.ofOpenNormal V).degree

The norm index of an abelian layer: [Kˣ : N_{L/K}(Lˣ)] = [L : K], the degree of the layer being the order of its Galois group G_K ⧸ V.

Composita and intersections

theorem TauCeti.ClassFieldTheory.localNormSubgroup_inf_of_isAbelian {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {V W : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) (hW : W.IsAbelianClassFieldLayer) : localNormSubgroup K (V ⊓ W) = localNormSubgroup K V ⊓ localNormSubgroup K W

Composita. For finite abelian extensions cut out by 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 subextension of the compositum, which can be larger than the compositum of the maximal abelian subextensions.

@[simp]

theorem TauCeti.ClassFieldTheory.localNormSubgroup_sup {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (V W : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : localNormSubgroup K (V ⊔ W) = localNormSubgroup K V ⊔ localNormSubgroup K W

Intersections. The norm subgroup of the intersection of the finite Galois extensions cut out by V and W, which is cut out by V ⊔ W, is the product 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.