The graded norm above a prime-degree ramification break

For a Galois extension L/K of prime degree ℓ with break t, the graded norm at every unit depth v > t is bijective. Unlike the calculation below the break, the surviving term in N(1 + x) is the trace, not N(x). The trace maps 𝓂[L] ^ ψℕ(v) onto 𝓂[K] ^ v, while the remaining terms lie in 𝓂[K] ^ (v + 1).

This supplies the successive approximation step for norm surjectivity above the break. It is a statement about successive quotients, not yet about surjectivity on entire unit groups.

References

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

theorem TauCeti.norm_one_add_sub_one_sub_trace_mem_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, ⋯⟩) {x : ↥(ValuativeRel.valuation L).integer} (hx : x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ LocalFieldsRamification.psiNat K L v) : (Algebra.norm ↥(ValuativeRel.valuation K).integer) (1 + x) - 1 - (Algebra.trace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ (v + 1)

Above a prime-degree break the norm is the trace to first order. For x at depth ψℕ(v) with v > t, the nonlinear terms in N(1 + x) vanish modulo 𝓂[K] ^ (v + 1).

theorem TauCeti.normGradedMap_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, ⋯⟩) : Function.Bijective ⇑(normGradedMap K L v)

The graded norm is bijective above the break. In a Galois extension of prime degree with an upper break at a natural number t, every graded norm at unit depth v > t is bijective. The source depth is the canonical integral inverse Herbrand value ψℕ(v).