Documentation

TauCeti.NumberTheory.LocalField.Norm.Basic

Norm valuations in finite local-field extensions #

This file computes the normalized valuation of a field norm in finite extensions of nonarchimedean local fields. Mapping the norm back to the extension field raises the original valuation to the extension degree. The intrinsic formula is v_K(N_{L/K}(x)) = f(L/K) v_L(x).

The formula is the valuation input to the norm-group criterion for unramified extensions, which TauCeti.NumberTheory.LocalField.Norm.Unramified.Basic combines with surjectivity of the norm on units to identify the entire norm group. Read on ideals rather than on elements, the same formula says that the norm image of the maximal ideal of π’ͺ[L] is the residue-degree power of the maximal ideal of π’ͺ[K].

Ideal norms are read through Mathlib's: the norm image of a principal ideal is Ideal.relNorm_singleton, and the norm image of the maximal ideal is Ideal.relNorm π’ͺ[K] 𝓂[L], the form in which the local discriminant ideal is written.

On the unit filtration the norm is contravariant to the algebra map, which carries U(K,i) into U(L, e(L/K) i): the norm carries U(L, e(L/K) i) into U(K,i), because 𝓂[L]^(e i) is the ideal generated by 𝓂[K]^i and the norm commutes with reduction modulo 𝓂[K]^i. Without the factor e(L/K) the inclusion is false for ramified extensions; the sharp statement carries a Herbrand shift instead.

Main results #

References #

source
theorem TauCeti.normalizedValuation_norm_eq_one_of_eq_one {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] [FiniteDimensional K L] (x : LΛ£) (hx : (normalizedValuation L) x = 1) :
(normalizedValuation K) ((Algebra.normUnits K) x) = 1

The norm of a valuation-zero unit has valuation zero in every finite local-field extension.

source
@[simp]
theorem TauCeti.normalizedValuation_norm {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] [FiniteDimensional K L] (x : LΛ£) :
(normalizedValuation K) ((Algebra.normUnits K) x) = (normalizedValuation L) x ^ inertiaDegree K L

Valuation of a norm in a finite local-field extension. The normalized valuation of N_{L/K}(x) is f(L/K) times the normalized valuation of x.

source
theorem TauCeti.normalizedValuation_algebraMap_norm {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] [FiniteDimensional K L] (x : LΛ£) :
(normalizedValuation L) ((Units.map ↑(algebraMap K L)) ((Algebra.normUnits K) x)) = (normalizedValuation L) x ^ Module.finrank K L

Valuation of a norm after scalar extension. This is the intrinsic norm formula multiplied by the ramification index, using e(L/K) f(L/K) = [L : K].

source
theorem TauCeti.toAdd_normalizedValuation_norm {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] [FiniteDimensional K L] (x : LΛ£) :
Multiplicative.toAdd ((normalizedValuation K) ((Algebra.normUnits K) x)) = ↑(inertiaDegree K L) * Multiplicative.toAdd ((normalizedValuation L) x)

Additive valuation of a norm in a finite local-field extension. This is v_K(N_{L/K}(x)) = f(L/K) v_L(x).

source
@[simp]
theorem TauCeti.normalizedValuationWithZero_norm {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] [FiniteDimensional K L] (x : L) :
(normalizedValuationWithZero K) ((Algebra.norm K) x) = (normalizedValuationWithZero L) x ^ inertiaDegree K L

Valuation of the field norm in a finite local-field extension, including zero.

source
@[simp]
theorem TauCeti.coe_norm_integerRing {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] (y : β†₯(ValuativeRel.valuation L).integer) :
↑((Algebra.norm β†₯(ValuativeRel.valuation K).integer) y) = (Algebra.norm K) ↑y

The norm of π’ͺ[L] over π’ͺ[K], a free module of finite rank, is the restriction of the field norm of L/K.

source
@[simp]
theorem TauCeti.coe_trace_integerRing {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] (y : β†₯(ValuativeRel.valuation L).integer) :
↑((Algebra.trace β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) y) = (Algebra.trace K L) ↑y

The trace of π’ͺ[L] over π’ͺ[K], a free module of finite rank, is the restriction of the field trace of L/K.

source
theorem TauCeti.norm_mem_integer {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] {y : L} (hy : y ∈ (ValuativeRel.valuation L).integer) :
(Algebra.norm K) y ∈ (ValuativeRel.valuation K).integer

The norm of an element of π’ͺ[L] lies in π’ͺ[K].

source
theorem TauCeti.relNorm_maximalIdeal_eq_maximalIdeal_pow (K : Type u_3) (L : Type u_4) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] :
(Ideal.relNorm β†₯(ValuativeRel.valuation K).integer) (IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation L).integer) = IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer ^ inertiaDegree K L

The ideal norm of the maximal ideal of π’ͺ[L] is the residue-degree power of the maximal ideal of π’ͺ[K]: N_{L/K}(𝓂[L]) = 𝓂[K] ^ f(L/K), in the form of Mathlib's Ideal.relNorm.

This is the ideal-theoretic form of TauCeti.toAdd_normalizedValuation_norm, the valuation of a norm being f(L/K) times the valuation of its argument: a uniformizer of π’ͺ[L] is taken to an element of π’ͺ[K] of normalized valuation f(L/K), which generates 𝓂[K] ^ f(L/K) in the discrete valuation ring π’ͺ[K]. The principal-ideal step reads off Ideal.relNorm_singleton.

source
theorem TauCeti.norm_mem_maximalIdeal_pow_of_mem (K : Type u_3) {L : Type u_4} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {m : β„•} {x : β†₯(ValuativeRel.valuation L).integer} (hx : x ∈ IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation L).integer ^ m) :
(Algebra.norm β†₯(ValuativeRel.valuation K).integer) x ∈ IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer ^ (inertiaDegree K L * m)

The norm of an element of 𝓂[L] ^ m lies in 𝓂[K] ^ (f(L/K) m).

source
theorem TauCeti.normUnits_mem_unitFiltration_zero_iff {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] [FiniteDimensional K L] {y : LΛ£} :
(Algebra.normUnits K) y ∈ unitFiltration K 0 ↔ y ∈ unitFiltration L 0

A unit of L is a unit of π’ͺ[L] exactly when its norm is a unit of π’ͺ[K].

source
theorem TauCeti.normUnits_mem_unitFiltration_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] {i : β„•} {y : LΛ£} (hy : y ∈ unitFiltration L (ramificationIndex K L * i)) :
(Algebra.normUnits K) y ∈ unitFiltration K i

The norm carries U(L, e(L/K) i) into U(K, i). A unit of π’ͺ[L] congruent to 1 modulo 𝓂[L]^(e i) = 𝓂[K]^i π’ͺ[L] has norm congruent to 1 modulo 𝓂[K]^i, because the norm commutes with reduction modulo 𝓂[K]^i.

source
theorem TauCeti.map_normUnits_unitFiltration_le (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] (i : β„•) :
Subgroup.map (Algebra.normUnits K) (unitFiltration L (ramificationIndex K L * i)) ≀ unitFiltration K i

The norm carries U(L, e(L/K) i) into U(K, i), as an inclusion of subgroups of KΛ£. At i = 0 this says that the norm of a unit of π’ͺ[L] is a unit of π’ͺ[K].

source
theorem TauCeti.continuous_normUnits (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] :
Continuous ⇑(Algebra.normUnits K)

The norm on unit groups of compatible local-field extensions is continuous.

source
theorem TauCeti.isUniformizer_normUnits_iff {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] [FiniteDimensional K L] {Ο– : LΛ£} (hΟ– : IsUniformizer L Ο–) :
IsUniformizer K ((Algebra.normUnits K) Ο–) ↔ inertiaDegree K L = 1

The norm of a uniformizer of L is a uniformizer of K exactly when the residue degree is 1, that is when L/K is totally ramified.

source
theorem TauCeti.irreducible_norm_iff_inertiaDegree_eq_one_of_irreducible {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] {ΞΎ : β†₯(ValuativeRel.valuation L).integer} (hΞΎ : Irreducible ΞΎ) :
Irreducible ((Algebra.norm β†₯(ValuativeRel.valuation K).integer) ΞΎ) ↔ inertiaDegree K L = 1

The norm of an irreducible element of π’ͺ[L] is irreducible in π’ͺ[K] exactly when the residue degree of L/K is one.

source
theorem TauCeti.addVal_norm {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] (z : β†₯(ValuativeRel.valuation L).integer) :
(IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation K).integer) ((Algebra.norm β†₯(ValuativeRel.valuation K).integer) z) = inertiaDegree K L β€’ (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation L).integer) z

The valuation of a norm: v_K(N_{L/K}(z)) = f(L/K) v_L(z) for every z ∈ π’ͺ[L], read on the additive valuations of the discrete valuation rings π’ͺ[K] and π’ͺ[L].

source
theorem TauCeti.inertiaDegree_dvd_of_mem_normGroup {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] [FiniteDimensional K L] {x : Kˣ} (hx : x ∈ normGroup K L) :
↑(inertiaDegree K L) ∣ Multiplicative.toAdd ((normalizedValuation K) x)

The normalized valuation of an element of the norm group N_{L/K}(LΛ£) is divisible by the residue degree f(L/K).

source
theorem TauCeti.comap_zmultiples_inertiaDegree_le_normGroup {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] [FiniteDimensional K L] (hU : unitFiltration K 0 ≀ normGroup K L) :
Subgroup.comap (normalizedValuation K) (AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑(inertiaDegree K L))) ≀ normGroup K L

If the units of K are norms from L, then the norm group contains every element of KΛ£ whose valuation is divisible by the residue degree f(L/K): such an element is a power of the norm of a uniformizer of L times a unit.

source
theorem TauCeti.algebraMap_norm_integerRing_eq_prod_automorphisms {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] [FiniteDimensional K L] [IsGalois K L] (z : β†₯(ValuativeRel.valuation L).integer) :
(algebraMap β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) ((Algebra.norm β†₯(ValuativeRel.valuation K).integer) z) = ∏ Οƒ : Gal(L/K), Οƒ β€’ z

In a Galois extension, the norm of an integer z of L, read in π’ͺ[L], is the product of the Galois conjugates of z.

source
theorem TauCeti.algebraMap_trace_integerRing_eq_sum_automorphisms {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] [FiniteDimensional K L] [IsGalois K L] (z : β†₯(ValuativeRel.valuation L).integer) :
(algebraMap β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) ((Algebra.trace β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) z) = βˆ‘ Οƒ : Gal(L/K), Οƒ β€’ z

In a Galois extension, the trace of an integer z of L, read in π’ͺ[L], is the sum of the Galois conjugates of z.