The trace of the powers of the maximal ideal of a local field extension

Let L/K be a finite separable extension of nonarchimedean local fields, with ramification index e = e(L/K) and different exponent d = d(L/K). This file computes the image of the powers of the maximal ideal of 𝒪[L] under the integral trace Tr = Algebra.intTrace 𝒪[K] 𝒪[L]:

Tr(𝓂[L] ^ m) = 𝓂[K] ^ ((m + d) / e),

with the division of natural numbers. It is the specialization of TauCeti.map_intTrace_pow_eq_maximalIdeal_pow to the discrete valuation rings 𝒪[K] and 𝒪[L], where 𝓂[K] · 𝒪[L] = 𝓂[L] ^ e. At m = 0 it says that the trace maps 𝒪[L] onto 𝒪[K] exactly when d < e, that is, exactly when L/K is tamely ramified.

The formula is the input to the computation of the norm on the unit filtration: the expansion N(1 + x) = 1 + Tr(x) + ⋯ + N(x) for x ∈ 𝓂[L] ^ m has trace terms whose valuations it bounds (Serre, Local Fields, Chapter V, §3).

Main results

• TauCeti.map_intTrace_maximalIdeal_pow: Tr(𝓂[L] ^ m) = 𝓂[K] ^ ((m + d(L/K)) / e(L/K)).
• TauCeti.intTrace_mem_maximalIdeal_pow_of_mem: the element form, Tr(x) ∈ 𝓂[K] ^ r for x ∈ 𝓂[L] ^ m whenever e(L/K) r ≤ m + d(L/K).
• TauCeti.range_intTrace: Tr(𝒪[L]) = 𝓂[K] ^ (d(L/K) / e(L/K)).
• TauCeti.intTrace_surjective_iff_isTamelyRamified: the trace maps 𝒪[L] onto 𝒪[K] exactly when L/K is tamely ramified.

References

• J.-P. Serre, Local Fields, Chapter III (the different) and Chapter V, §3.

@[simp]

theorem TauCeti.map_intTrace_maximalIdeal_pow (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] [Algebra.IsSeparable K L] (m : ℕ) : Submodule.map (Algebra.intTrace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) (Submodule.restrictScalars (↥(ValuativeRel.valuation K).integer) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ m)) = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ ((m + differentExponent K L) / ramificationIndex K L)

The trace of a power of the maximal ideal: the integral trace carries 𝓂[L] ^ m onto 𝓂[K] ^ ((m + d(L/K)) / e(L/K)), with the division of natural numbers.

theorem TauCeti.intTrace_mem_maximalIdeal_pow_of_mem {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] [Algebra.IsSeparable K L] {m r : ℕ} {x : ↥(ValuativeRel.valuation L).integer} (hx : x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ m) (h : ramificationIndex K L * r ≤ m + differentExponent K L) : (Algebra.intTrace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ r

The integral trace of an element of 𝓂[L] ^ m lies in 𝓂[K] ^ r as soon as e(L/K) r ≤ m + d(L/K).

@[simp]

theorem TauCeti.range_intTrace (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] [Algebra.IsSeparable K L] : (Algebra.intTrace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer).range = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ (differentExponent K L / ramificationIndex K L)

The trace of the ring of integers: the image of 𝒪[L] under the integral trace is 𝓂[K] ^ (d(L/K) / e(L/K)).

@[simp]

theorem TauCeti.intTrace_surjective_iff_isTamelyRamified (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] [Algebra.IsSeparable K L] : Function.Surjective ⇑(Algebra.intTrace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) ↔ IsTamelyRamified K L

The trace is surjective exactly in the tame case: the integral trace maps 𝒪[L] onto 𝒪[K] if and only if L/K is tamely ramified.