Local norm subgroups

An open normal subgroup V of the absolute Galois group of a nonarchimedean local field cuts out the finite Galois extension classField K V. This file attaches to V the concrete norm subgroup N_{classField K V/K}(classField K V)ˣ of Kˣ, identifies it with the norm subgroup of the local class formation, and proves its order-theoretic properties.

The topology statement is inherited from the local inverse-function theorem for the field norm; finite index follows from the valuation--unit decomposition of Kˣ. The order-theoretic properties are those of the norm subgroups Formation.normSubgroup of the units formation, read on Kˣ through the order isomorphism localGroundOrderIso: monotonicity in V comes from the transitivity of the formation norm, and norm limitation shows that replacing V by its maximal abelian sublayer does not change the subgroup.

Main definitions

• TauCeti.ClassFieldTheory.localNormSubgroup: the norm subgroup of the class field cut out by an open normal subgroup of the absolute Galois group.
• TauCeti.ClassFieldTheory.localGroundEquiv: the identification of Kˣ, written additively, with the ground level of a finite layer of the units formation.
• TauCeti.ClassFieldTheory.localGroundOrderIso: the identification of the subgroups of Kˣ with the subgroups of the ground level of the units formation, carrying localNormSubgroup to Formation.normSubgroup.

Main results

• TauCeti.ClassFieldTheory.isOpen_localNormSubgroup: local norm subgroups are open.
• TauCeti.ClassFieldTheory.finiteIndex_localNormSubgroup: local norm subgroups have finite index.
• TauCeti.ClassFieldTheory.localNormSubgroup_mono: inclusion of layer subgroups gives inclusion of norm subgroups.
• TauCeti.ClassFieldTheory.localNormSubgroup_maximalAbelianLayer: a layer and its maximal abelian sublayer have the same norm subgroup.
• TauCeti.ClassFieldTheory.localNormSubgroup_top: the ground field has norm subgroup Kˣ.

References

• J.-P. Serre, Local Fields, Chapter V, §2.
• J. Neukirch, Algebraic Number Theory, Chapter II, §5.

noncomputable def TauCeti.ClassFieldTheory.localNormSubgroup (K : Type u_1) [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : Subgroup Kˣ

The local norm subgroup cut out by an open normal subgroup. It is the image in Kˣ of the field norm from the finite Galois extension classField K V.

theorem TauCeti.ClassFieldTheory.localNormSubgroup_def (K : Type u_1) [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : localNormSubgroup K V = normGroup K ↥(classField K V)

The local norm subgroup of V is the norm group of the class field classField K V.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_localNormSubgroup_iff (K : Type u_1) [Field K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} {x : Kˣ} : x ∈ localNormSubgroup K V ↔ ∃ (y : (↥(classField K V))ˣ), (Algebra.norm K) ↑y = ↑x

Membership in a local norm subgroup means being the norm of a nonzero element of the corresponding class field.

theorem TauCeti.ClassFieldTheory.isOpen_localNormSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : IsOpen ↑(localNormSubgroup K V)

Local norm subgroups are open.

theorem TauCeti.ClassFieldTheory.finiteIndex_localNormSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : (localNormSubgroup K V).FiniteIndex

Local norm subgroups have finite index.

Comparison with the units formation

noncomputable def TauCeti.ClassFieldTheory.localGroundEquiv (K : Type) [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : Additive Kˣ ≃+ ↥((unitsFormation K).level (NormalLayer.ofOpenNormal V).ground)

The ground level of the layer V ◁ G_K of the units formation is Kˣ, written additively. This identification moves no element of the separable closure.

@[simp]

theorem TauCeti.ClassFieldTheory.localGroundEquiv_apply_coe (K : Type) [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (x : Additive Kˣ) : ↑((localGroundEquiv K V) x) = (unitsCoeffEquivUnitsFormation K) (Additive.ofMul ((Units.map ↑(Algebra.ofId K (SeparableClosure K))) (Additive.toMul x)))

localGroundEquiv sends a unit of K to the same unit in the coefficient module of the units formation.

theorem TauCeti.ClassFieldTheory.groundEquivOfOpenNormal_unitsLevelEquiv (K : Type) [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (x : Kˣ) : (NormalLayer.groundEquivOfOpenNormal (unitsFormation K) V) ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul x)) = (localGroundEquiv K V) (Additive.ofMul x)

The unit x ∈ Kˣ, as an element of the ground level of the top layer, read in the ground level of the layer V ◁ G_K, is localGroundEquiv K V x.

theorem TauCeti.ClassFieldTheory.localGroundEquiv_mem_normSubgroup_iff (K : Type) [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (x : Kˣ) : (localGroundEquiv K V) (Additive.ofMul x) ∈ (NormalLayer.ofOpenNormal V).normSubgroup (unitsFormation K) ↔ x ∈ localNormSubgroup K V

Under localGroundEquiv, the concrete local norm subgroup is the norm subgroup of the corresponding layer of the units formation.

noncomputable def TauCeti.ClassFieldTheory.localGroundOrderIso (K : Type) [Field K] : Subgroup Kˣ ≃o Submodule ℤ ↥((unitsFormation K).level ⊤)

Subgroups of Kˣ are the subgroups of the ground level of the units formation. The level of the whole group G_K is Kˣ, written additively, so taking preimages along that identification is an order isomorphism. It carries the concrete local norm subgroups to the norm subgroups of the units formation (localGroundOrderIso_localNormSubgroup), which transports the lattice laws of the norm subgroups of a class formation to Kˣ.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_localGroundOrderIso (K : Type) [Field K] {H : Subgroup Kˣ} {a : ↥((unitsFormation K).level ⊤)} : a ∈ (localGroundOrderIso K) H ↔ Additive.toMul ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯).symm a) ∈ H

An element of the ground level lies in the image of a subgroup H ≤ Kˣ under localGroundOrderIso exactly when the corresponding unit of K lies in H.

@[simp]

theorem TauCeti.ClassFieldTheory.localGroundOrderIso_localNormSubgroup (K : Type) [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : (localGroundOrderIso K) (localNormSubgroup K V) = (unitsFormation K).normSubgroup V

localGroundOrderIso carries the local norm subgroup of V to the norm subgroup of the layer V ◁ G_K of the units formation.

Order properties

theorem TauCeti.ClassFieldTheory.localNormSubgroup_mono (K : Type) [Field K] : Monotone (localNormSubgroup K)

Local norm subgroups are monotone in the layer subgroup. If V ≤ W, then the class field of W is contained in that of V, and every norm from the larger field is a norm from the smaller field.

@[simp]

theorem TauCeti.ClassFieldTheory.localNormSubgroup_top (K : Type) [Field K] : localNormSubgroup K ⊤ = ⊤

The top layer has the whole unit group as its norm subgroup. It cuts out the ground field itself, whose norm to itself is the identity. This pins the direction of the local class-field correspondence.

theorem TauCeti.ClassFieldTheory.localNormSubgroup_maximalAbelianLayer (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : localNormSubgroup K V.maximalAbelianLayer = localNormSubgroup K V

Concrete norm limitation. A finite Galois extension of a nonarchimedean local field and its maximal abelian subextension have the same norm subgroup.