Norm surjectivity above a ramification break

Surjectivity of the successive graded norms implies surjectivity on an entire unit-filtration step. The image of the source step is compact, hence closed, and successive approximation makes it dense in the target step. Thus no choice of an infinite product is needed.

For a Galois extension of prime degree with upper break t, this proves N(U(L, ψℕ(v))) = U(K,v) whenever t < v. The depths are the canonical integral inverse Herbrand values, so the result includes wild extensions without removing the Herbrand shift.

References

• J.-P. Serre, Corps Locaux, Chapter V, §3, Proposition 5 and its corollaries.

theorem TauCeti.map_normUnits_unitFiltration_eq_of_surjective_normGradedMap {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] [Module.Finite K L] [IsGalois K L] (v : ℕ) (h : ∀ (n : ℕ), v ≤ n → Function.Surjective ⇑(normGradedMap K L n)) : Subgroup.map (Algebra.normUnits K) (unitFiltration L (LocalFieldsRamification.psiNat K L v)) = unitFiltration K v

Surjectivity of every graded norm at and beyond v implies surjectivity of the norm from U(L, ψℕ(v)) onto U(K,v).

theorem TauCeti.map_normUnits_unitFiltration_after_break {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] [Module.Finite K L] [IsGalois K L] (hℓ : Nat.Prime (Module.finrank K L)) {t v : ℕ} (hvt : t < v) (ht : LocalFieldsRamification.UpperJump K L ⟨↑t, ⋯⟩) : Subgroup.map (Algebra.normUnits K) (unitFiltration L (LocalFieldsRamification.psiNat K L v)) = unitFiltration K v

The norm is surjective on every unit step above a prime-degree break. For a Galois extension of prime degree with an upper break at a natural number t, the norm maps U(L, ψℕ(v)) onto U(K,v) whenever t < v.