The different exponent of an extension of local fields #

Let L/K be a separable extension of nonarchimedean local fields whose valuations are compatible, in the sense of ValuativeExtension K L. The different ideal 𝔡(L/K) of Mathlib's differentIdeal 𝒪[K] 𝒪[L] is a nonzero ideal of the discrete valuation ring 𝒪[L], hence a power of its maximal ideal. This file defines the exponent,

TauCeti.differentExponent K L : ℕ,

so that 𝔡(L/K) = 𝓂[L] ^ d(L/K), and compares it with the ramification index e = e(L/K):

e - 1 ≤ d(L/K) always;
d(L/K) = e - 1 exactly when L/K is tamely ramified (TauCeti.IsTamelyRamified), that is, when the residue characteristic does not divide e;
e ≤ d(L/K) exactly when L/K is wildly ramified (TauCeti.IsWildlyRamified);
d(L/K) = 0 exactly when L/K is unramified.

These are the local form of Dedekind's different theorem. The residue fields of local fields are finite, so the residue extension is always separable and tameness is a condition on e alone.

Main definitions #

TauCeti.differentExponent: the exponent d(L/K) of the maximal ideal of 𝒪[L] in the different ideal.

Main results #

TauCeti.isSeparable_fractionRing_integerRing: separability of L/K in the form taken by Mathlib's different ideal, on the fraction fields of 𝒪[K] and 𝒪[L].
TauCeti.pow_dvd_differentIdeal_iff_le_differentExponent: the characteristic property, 𝓂[L] ^ n ∣ 𝔡(L/K) ↔ n ≤ d(L/K).
TauCeti.differentIdeal_eq_maximalIdeal_pow: 𝔡(L/K) = 𝓂[L] ^ d(L/K).
TauCeti.ramificationIndex_sub_one_le_differentExponent: e - 1 ≤ d(L/K).
TauCeti.ramificationIndex_le_differentExponent_iff: e ≤ d(L/K) exactly in the wild case.
TauCeti.differentExponent_eq_ramificationIndex_sub_one_iff: d(L/K) = e - 1 exactly in the tame case.
TauCeti.differentExponent_eq_zero_iff and TauCeti.differentIdeal_eq_top_iff: the different is trivial exactly when L/K is unramified.

References #

J.-P. Serre, Corps Locaux, Chapter III, §6, Proposition 13.
J. Neukirch, Algebraic Number Theory, Chapter III, Theorem 2.6.

source

instance TauCeti.isSeparable_fractionRing_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] [Algebra.IsSeparable K L] :

Algebra.IsSeparable (FractionRing ↥(ValuativeRel.valuation K).integer) (FractionRing ↥(ValuativeRel.valuation L).integer)

Separability of L / K transported to the canonical fraction fields of 𝒪[K] and 𝒪[L], which is the form of the hypothesis taken by Mathlib's theory of the different ideal.

source

noncomputable def TauCeti.differentExponent (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] :

ℕ

The different exponent d(L/K) of an extension of nonarchimedean local fields: the multiplicity of the maximal ideal of 𝒪[L] in the different ideal differentIdeal 𝒪[K] 𝒪[L]. For L/K separable the different ideal is 𝓂[L] ^ d(L/K), by differentIdeal_eq_maximalIdeal_pow.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem TauCeti.differentExponent_def (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] :

differentExponent K L = multiplicity (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer) (differentIdeal ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer)

The defining formula of differentExponent.

source

@[simp]

theorem TauCeti.pow_dvd_differentIdeal_iff_le_differentExponent (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] {n : ℕ} :

IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ n ∣ differentIdeal ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer ↔ n ≤ differentExponent K L

The characteristic property of the different exponent: the n-th power of the maximal ideal of 𝒪[L] divides the different ideal exactly when n ≤ d(L/K).

source

theorem TauCeti.differentIdeal_eq_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] :

differentIdeal ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ differentExponent K L

The different ideal of a separable extension of nonarchimedean local fields is the d(L/K)-th power of the maximal ideal of 𝒪[L].

source

theorem TauCeti.ramificationIndex_sub_one_le_differentExponent (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] :

ramificationIndex K L - 1 ≤ differentExponent K L

The first half of Dedekind's different theorem: e(L/K) - 1 ≤ d(L/K).

source

@[simp]

theorem TauCeti.ramificationIndex_le_differentExponent_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] [Algebra.IsSeparable K L] :

ramificationIndex K L ≤ differentExponent K L ↔ IsWildlyRamified K L

The different exponent reaches the ramification index exactly in the wild case: e(L/K) ≤ d(L/K) if and only if the residue characteristic divides e(L/K).

source

@[simp]