The norm of 1 + x in a Galois extension of prime degree

Let L/K be a Galois extension of nonarchimedean local fields of prime degree ℓ, so that its Galois group is cyclic of order ℓ, and let x ∈ 𝓂[L]^m. Expanding the norm N_{L/K}(1 + x) = ∏_σ (1 + σ x) gives the sum, over the subsets S of the Galois group, of the products ∏_{σ ∈ S} σ x. Because the group has prime order, it permutes the subsets with at least two elements, other than the whole group, freely, so these terms collect into the trace of an element y of 𝓂[L]^(2m), and

N_{L/K}(1 + x) = 1 + Tr_{L/K}(x) + Tr_{L/K}(y) + N_{L/K}(x).

This is the shape in which the norm is computed on the unit filtration of such an extension: the valuations of the two traces are read off from the behaviour of the trace on powers of the maximal ideal, and v_K(N_{L/K}(x)) = f(L/K) v_L(x), which is v_L(x) when the extension is totally ramified and ℓ v_L(x) when it is unramified. It is Lemma 5 of Serre, Local Fields, Chapter V, §3, stated for the integer rings.

Main results

• TauCeti.exists_norm_one_add_eq_of_mem_maximalIdeal_pow: the expansion above.

References

• J.-P. Serre, Local Fields, Chapter V, §3, Lemma 5.

theorem TauCeti.exists_norm_one_add_eq_of_mem_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] [IsGalois K L] (hℓ : Nat.Prime (Module.finrank K L)) {m : ℕ} {x : ↥(ValuativeRel.valuation L).integer} (hx : x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ m) : ∃ y ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ (2 * m), (Algebra.norm ↥(ValuativeRel.valuation K).integer) (1 + x) = 1 + (Algebra.trace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) x + (Algebra.trace ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) y + (Algebra.norm ↥(ValuativeRel.valuation K).integer) x

The norm of 1 + x in a Galois extension of prime degree (Serre, Local Fields, V §3, Lemma 5). If L/K is a Galois extension of nonarchimedean local fields of prime degree and x ∈ 𝓂[L]^m, then there is y ∈ 𝓂[L]^(2m) with

N_{L/K}(1 + x) = 1 + Tr_{L/K}(x) + Tr_{L/K}(y) + N_{L/K}(x),

the norm and trace being those of 𝒪[L] over 𝒪[K].