Local existence

Let K be a nonarchimedean local field and n a natural number invertible in K. Every subgroup of Kˣ containing the n-th powers is the norm subgroup of a finite abelian extension (exists_abelianLayer_localNormSubgroup_eq_of_powerSubgroup_le). Since a subgroup of index n contains the n-th powers, this gives local existence: for K of characteristic zero, in particular for a finite extension of ℚ_p, every subgroup of finite index of Kˣ is the norm subgroup of a finite abelian extension (localAbelianExistence), and the same holds in every characteristic for subgroups of index prime to the residue characteristic (localAbelianExistence_primeToResidueCharacteristic). Such a subgroup is automatically open, because it contains the open subgroup (Kˣ)ⁿ; the existence theorems therefore carry no openness hypothesis.

By the upward closure of norm subgroups (exists_abelianLayer_localNormSubgroup_eq_of_normGroup_le) it suffices to find one finite separable extension whose norm group consists of n-th powers.

• Kummer step. If K contains a primitive n-th root of unity, adjoin to K an n-th root of a representative of each of the finitely many classes of Kˣ/(Kˣ)ⁿ. A norm a from the resulting field E is a norm from each cyclic Kummer extension K(ⁿ√b), so its Hilbert symbol (a, b) vanishes for every b (localSymbol_eq_zero_iff_mem_normGroup); by antisymmetry and the nondegeneracy of the Hilbert pairing (forall_localSymbol_kummerClass_eq_zero_iff), a is an n-th power.
• Descent. In general, run the Kummer step over K' = K(μₙ). The norm from the resulting field to K factors through K', and the norm K'ˣ → Kˣ carries n-th powers to n-th powers.

The proof uses local reciprocity, the Hilbert pairing and the finiteness of Kˣ/(Kˣ)ⁿ; it does not use Lubin–Tate theory.

Main results

• TauCeti.ClassFieldTheory.exists_abelianLayer_localNormSubgroup_eq_of_powerSubgroup_le: for n invertible in K, a subgroup of Kˣ containing (Kˣ)ⁿ is the norm subgroup of an abelian layer.
• TauCeti.ClassFieldTheory.localAbelianExistence: in characteristic zero, every subgroup of finite index of Kˣ is the norm subgroup of an abelian layer.
• TauCeti.ClassFieldTheory.localExistence: its forgetful form.
• TauCeti.ClassFieldTheory.localAbelianExistence_primeToResidueCharacteristic: every subgroup of finite index prime to the residue characteristic is the norm subgroup of an abelian layer.
• TauCeti.ClassFieldTheory.localExistence_primeToResidueCharacteristic: its forgetful form.

References

• J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chapter XIV, §6, the existence theorem through the Hilbert symbol.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §6.

theorem TauCeti.ClassFieldTheory.exists_abelianLayer_localNormSubgroup_eq_of_powerSubgroup_le {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : ↑n ≠ 0) {N : Subgroup Kˣ} (h : powerSubgroup Kˣ n ≤ N) : ∃ (W : OpenNormalSubgroup (AbsoluteGaloisGroup K)), W.IsAbelianClassFieldLayer ∧ localNormSubgroup K W = N

Local existence for subgroups containing the n-th powers. For a nonarchimedean local field K and n invertible in K, every subgroup of Kˣ containing (Kˣ)ⁿ is the norm subgroup of a finite abelian extension. No root of unity in K is needed.

theorem TauCeti.ClassFieldTheory.localAbelianExistence {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] (N : Subgroup Kˣ) [N.FiniteIndex] : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), V.IsAbelianClassFieldLayer ∧ localNormSubgroup K V = N

Local existence in characteristic zero. For a nonarchimedean local field K of characteristic zero, in particular a finite extension of ℚ_p, every subgroup of finite index of Kˣ is the norm subgroup of a finite abelian extension. Such a subgroup is open, as it contains the open subgroup of [Kˣ : N]-th powers.

theorem TauCeti.ClassFieldTheory.localExistence {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] (N : Subgroup Kˣ) [N.FiniteIndex] : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), localNormSubgroup K V = N

Local existence in characteristic zero, forgetful form. Some open normal subgroup, not necessarily an abelian layer, has the given norm subgroup. By norm limitation, replacing a layer by its maximal abelian sublayer does not change its norm subgroup.

theorem TauCeti.ClassFieldTheory.localAbelianExistence_primeToResidueCharacteristic {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] (N : Subgroup Kˣ) (hindex : N.index.Coprime p) : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), V.IsAbelianClassFieldLayer ∧ localNormSubgroup K V = N

Local existence prime to the residue characteristic. For a nonarchimedean local field K with residue field of characteristic p, whether K itself has characteristic 0 or p, every subgroup of Kˣ of index prime to p is the norm subgroup of a finite abelian extension. The coprimality forces the index to be finite, as Nat.Coprime 0 p fails.

theorem TauCeti.ClassFieldTheory.localExistence_primeToResidueCharacteristic {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] (N : Subgroup Kˣ) (hindex : N.index.Coprime p) : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), localNormSubgroup K V = N

Local existence prime to the residue characteristic, forgetful form.