The trace below the Herbrand shift

Let L/K be a finite Galois extension of nonarchimedean local fields. Hilbert's formula d(L/K) = ∑_{i ≥ 0} (#G_i - 1), truncated at m = ψℕ_{L/K}(n), together with the defining identity #G_1 + ⋯ + #G_m = n · #G_0, gives

e(L/K) (n + 1) ≤ ψℕ_{L/K}(n) + 1 + d(L/K).

The trace formula for powers of the maximal ideal then bounds the integral trace below the Herbrand shift. This is the trace input to the Herbrand-shifted norm inclusion in TauCeti.NumberTheory.LocalField.Norm.Herbrand.

Main results

• TauCeti.intTrace_mem_maximalIdeal_pow_succ_of_mem_psiNat: the integral trace carries 𝓂[L] ^ (ψℕ_{L/K}(n) + 1) into 𝓂[K] ^ (n + 1).
• TauCeti.trace_mem_maximalIdeal_pow_succ: when [L : K] ≥ 2 and G_{v+1} = Gal(L/K), the trace carries 𝓂[L] ^ v into 𝓂[K] ^ (v + 1).

References

• J.-P. Serre, Corps Locaux, Chapter V, §3 (Lemmas 4 and 5) and §6 (Proposition 8).

theorem TauCeti.intTrace_mem_maximalIdeal_pow_succ_of_mem_psiNat {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] {n : ℕ} {x : ↥(ValuativeRel.valuation L).integer} (hx : x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ (LocalFieldsRamification.psiNat K L n + 1)) : (Algebra.intTrace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ (n + 1)

The trace below the Herbrand shift. In a finite Galois extension L/K of nonarchimedean local fields, the integral trace carries 𝓂[L] ^ (ψℕ_{L/K}(n) + 1) into 𝓂[K] ^ (n + 1).

theorem TauCeti.trace_mem_maximalIdeal_pow_succ {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] (h2 : 2 ≤ Module.finrank K L) {v : ℕ} (hG : LocalFieldsRamification.lowerRamificationGroup K L (↑v + 1) = ⊤) {w : ↥(ValuativeRel.valuation L).integer} (hw : w ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ v) : (Algebra.trace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) w ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ (v + 1)

If [L : K] ≥ 2 and G_{v+1} = Gal(L/K), the trace carries 𝓂[L] ^ v into 𝓂[K] ^ (v + 1): Hilbert's formula, truncated at v + 1, gives d(L/K) ≥ (v + 2) ([L : K] - 1).