Open norm groups of finite local-field extensions

The norm group of a finite separable extension of nonarchimedean local fields is open and has finite index. Openness is a local property of the field norm. Choose an element of trace one and restrict the norm to the affine line through 1 in that direction. This one-variable polynomial has derivative 1 at the origin, so the inverse function theorem shows that its image contains a neighbourhood of 1.

For finite index, the valuation--unit decomposition Kˣ ≃ ℤ × 𝒪[K]ˣ separates the two parts. The norm group contains a deep open unit-filtration subgroup, while norms of elements from the base field contain the degree multiples in the valuation factor. Their product has finite index.

Main results

• TauCeti.isOpen_normGroup: N_{L/K}(Lˣ) is open in Kˣ.
• TauCeti.exists_unitFiltration_le_normGroup: N_{L/K}(Lˣ) contains a step of the unit filtration.
• TauCeti.finiteIndex_normGroup: N_{L/K}(Lˣ) has finite index in Kˣ.

References

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

theorem TauCeti.isOpen_normGroup {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : IsOpen ↑(normGroup K L)

Norm groups of finite separable local-field extensions are open.

theorem TauCeti.exists_unitFiltration_le_normGroup {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : ∃ (n : ℕ), unitFiltration K n ≤ normGroup K L

The norm group of a finite separable local-field extension contains a step U(K,n) of the unit filtration.

theorem TauCeti.finiteIndex_normGroup {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : (normGroup K L).FiniteIndex

Norm groups of finite separable local-field extensions have finite index.