Norms in unramified extensions of local fields

Let L/K be a finite unramified extension of nonarchimedean local fields. This file proves that the norm maps every step of the unit filtration of L onto the corresponding step of the unit filtration of K,

N_{L/K}(U(L,i)) = U(K,i) for every i : ℕ,

and deduces the norm-equation criterion: an element x of Kˣ is a norm from L exactly when the residue degree f(L/K) divides v_K(x). So N_{L/K}(Lˣ) = π^{fℤ} × 𝒪[K]ˣ for any uniformizer π of K, in the form that decides the norm equation one element at a time.

The inclusion N_{L/K}(U(L,i)) ⊆ U(K,i) is the case e(L/K) = 1 of the general inclusion N_{L/K}(U(L, e i)) ⊆ U(K, i). Surjectivity is Hensel's lemma for the norm (TauCeti.Algebra.exists_norm_eq_of_norm_sub_mem), applied to the finite free 𝒪[K]-algebra 𝒪[L], which is Henselian at every positive power of 𝓂[K]. Its residual inputs hold because 𝓂[K] 𝒪[L] = 𝓂[L], so that 𝒪[L] ⧸ 𝓂[K] 𝒪[L] is the residue field of L, a finite extension of the finite residue field of K: the norm of a finite extension of finite fields is surjective, which supplies the approximate solution at depth 0, and its trace is surjective because the extension is separable, which supplies the unit of unit trace that Hensel's lemma needs. At positive depth i the approximate solution is 1, and Hensel's lemma at 𝓂[K]^i returns a solution congruent to 1 modulo 𝓂[K]^i 𝒪[L] = 𝓂[L]^i.

⚠ Both statements fail for ramified extensions: at L = ℚ_2(√2) the norms of the units of 𝒪[L] form a subgroup of index 2 in ℤ_2ˣ, and in general the norm carries U(L,i) only into a Herbrand-shifted step of the filtration of K.

Main results

• TauCeti.map_normUnits_unitFiltration: in an unramified extension the norm maps U(L,i) onto U(K,i), for every i.
• TauCeti.mem_normGroup_iff_dvd_normalizedValuation: in an unramified extension x ∈ Kˣ is a norm exactly when f(L/K) divides v_K(x).

References

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

@[simp]

theorem TauCeti.map_normUnits_unitFiltration (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsUnramified K L] (i : ℕ) : Subgroup.map (Algebra.normUnits K) (unitFiltration L i) = unitFiltration K i

The norm is surjective on every step of the unit filtration in an unramified extension. If L/K is unramified, the norm maps U(L,i) onto U(K,i) for every i : ℕ: N_{L/K}(U(L,i)) = U(K,i). At i = 0 this is the surjectivity of the norm on units.

theorem TauCeti.mem_normGroup_iff_dvd_normalizedValuation {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsUnramified K L] {x : Kˣ} : x ∈ normGroup K L ↔ ↑(inertiaDegree K L) ∣ Multiplicative.toAdd ((normalizedValuation K) x)

The norm-equation criterion in an unramified extension. If L/K is unramified, an element x of Kˣ is a norm from L exactly when the residue degree f(L/K) divides v_K(x).