The local discriminant of an extension of local fields

The different 𝔡(L/K) of Mathlib is an ideal of 𝒪[L], the ring of integers of the upper field of an extension L/K of nonarchimedean local fields. The discriminant 𝔩(L/K) of the same extension is an ideal of the base ring 𝒪[K]: it is the norm image N_{L/K}(𝔡(L/K)), which is Tau Ceti's relDiscr 𝒪[K] 𝒪[L], the relative discriminant of the two rings of integers, and is built from Mathlib's ideal norm Ideal.relNorm. The two ideals live in different rings and are not to be conflated: TauCeti.differentExponent reads the exponent of 𝔡(L/K) in the maximal ideal of 𝒪[L], and this file adds TauCeti.discriminantExponent K L, for L/K separable, the exponent δ(L/K) of the maximal ideal of 𝒪[K] in 𝔩(L/K).

TauCeti.discriminantExponent is read for L/K separable. The trace form of an inseparable extension is degenerate, so the different ideal, and with it the discriminant ideal, is the zero ideal, and multiplicity 𝓂 (⊥ : Ideal 𝒪[K]) = 0 whatever the maximal ideal: an ℕ-valued order of vanishing would there be 0 for every power of the maximal ideal. The definition and the results below therefore carry [Algebra.IsSeparable K L].

A norm multiplies valuations by the residue degree, by TauCeti.toAdd_normalizedValuation_norm, so Ideal.relNorm 𝒪[K] 𝓂[L] is 𝓂[K] ^ f(L/K) (TauCeti.relNorm_maximalIdeal_eq_maximalIdeal_pow). The discriminant ideal is then 𝔩(L/K) = 𝓂[K] ^ δ(L/K), the ideal form of the product formula δ(L/K) = f(L/K) · d(L/K) (TauCeti.discriminantExponent_eq_inertiaDegree_mul_differentExponent). Since for L/K separable TauCeti.differentExponent is 0 exactly for unramified extensions, the discriminant inherits the unramified criterion and the bound f(L/K) · (e(L/K) - 1) ≤ δ(L/K).

Main definitions

• TauCeti.discriminantIdeal: the local discriminant ideal 𝔩(L/K) = N_{L/K}(𝔡(L/K)), the relative discriminant relDiscr 𝒪[K] 𝒪[L] of the two rings of integers.
• TauCeti.discriminantExponent: the local discriminant exponent δ(L/K) of a separable extension, the multiplicity of 𝓂[K] in 𝔩(L/K).

Main results

• TauCeti.discriminantIdeal_def, TauCeti.discriminantExponent_def: the defining formulas.
• TauCeti.discriminantIdeal_eq_of_algEquiv and TauCeti.discriminantExponent_eq_of_algEquiv: invariance under equivalence of finite extensions over the base field.
• TauCeti.discriminantExponent_eq_inertiaDegree_mul_differentExponent: the product formula δ(L/K) = f(L/K) · d(L/K).
• TauCeti.discriminantIdeal_eq_maximalIdeal_pow: 𝔩(L/K) = 𝓂[K] ^ δ(L/K).
• TauCeti.pow_dvd_discriminantIdeal_iff_le_discriminantExponent: the characteristic property, 𝓂[K] ^ n ∣ 𝔩(L/K) ↔ n ≤ δ(L/K).
• TauCeti.discriminantIdeal_eq_top_iff and TauCeti.discriminantExponent_eq_zero_iff: the discriminant is trivial exactly when the extension is unramified.
• TauCeti.inertiaDegree_mul_ramificationIndex_sub_one_le_discriminantExponent: the local discriminant bound, f(L/K) · (e(L/K) - 1) ≤ δ(L/K).
• TauCeti.ramificationIndex_sub_one_le_discriminantExponent: the residue-degree-free form of that bound, e(L/K) - 1 ≤ δ(L/K).
• TauCeti.discriminantExponent_eq_inertiaDegree_mul_ramificationIndex_sub_one_iff: the tame value of the discriminant exponent.

References

• J.-P. Serre, Corps Locaux, Chapter III, §6, Proposition 13.
• J. Neukirch, Algebraic Number Theory, Chapter II, §8.

noncomputable def TauCeti.discriminantIdeal (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] : Ideal ↥(ValuativeRel.valuation K).integer

The local discriminant ideal 𝔩(L/K) = N_{L/K}(𝔡(L/K)) of an extension L/K of nonarchimedean local fields: the norm image of the different ideal, an ideal of the base ring 𝒪[K]. It is not the different ideal 𝔡(L/K), which is an ideal of 𝒪[L].

It is the relative discriminant relDiscr 𝒪[K] 𝒪[L] of the two rings of integers, the same carrier for any finite extension of Dedekind domains, named here for the local field extension.

Equations

• TauCeti.discriminantIdeal K L = TauCeti.relDiscr ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

theorem TauCeti.discriminantIdeal_def (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] : discriminantIdeal K L = (Ideal.relNorm ↥(ValuativeRel.valuation K).integer) (differentIdeal ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer)

The defining formula of the local discriminant ideal: the relative norm of the different ideal, in the form of TauCeti.relDiscr_def.

theorem TauCeti.discriminantIdeal_ne_bot (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] : discriminantIdeal K L ≠ ⊥

The local discriminant ideal of a separable extension of local fields is nonzero, being the norm of the nonzero different ideal: the norm of an ideal of a Dedekind domain is zero only for the zero ideal, by Ideal.relNorm_eq_bot_iff.

noncomputable def TauCeti.discriminantExponent (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] [Algebra.IsSeparable K L] : ℕ

The local discriminant exponent δ(L/K) of a separable extension L/K of nonarchimedean local fields: the order of vanishing of the discriminant ideal discriminantIdeal K L at the maximal ideal of 𝒪[K], the largest n with 𝓂[K] ^ n ∣ 𝔩(L/K).

The separability hypothesis belongs to the definition and not only to the theorems below. The trace form of an inseparable extension is degenerate, so the different ideal and with it 𝔩(L/K) is the zero ideal, and the multiplicity of a maximal ideal in the zero ideal is 0 whatever that maximal ideal is: an ℕ-valued order of vanishing of 𝔩(L/K) would then be 0 for every power of the maximal ideal and carry no information.

Equations

• TauCeti.discriminantExponent K L = Nat.find ⋯

theorem TauCeti.discriminantExponent_def (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] : discriminantExponent K L = multiplicity (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) (discriminantIdeal K L)

The defining formula of discriminantExponent: the order of vanishing of the discriminant ideal at the maximal ideal of the base ring is its multiplicity.

theorem TauCeti.discriminantExponent_eq_inertiaDegree_mul_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] : discriminantExponent K L = inertiaDegree K L * differentExponent K L

The product formula for the local discriminant exponent: δ(L/K) = f(L/K) · d(L/K), for L/K separable.

theorem TauCeti.discriminantIdeal_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] : discriminantIdeal K L = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ discriminantExponent K L

The local discriminant ideal is the δ(L/K)-th power of the maximal ideal of 𝒪[K]: 𝔩(L/K) = 𝓂[K] ^ δ(L/K), for L/K separable.

@[simp]

theorem TauCeti.pow_dvd_discriminantIdeal_iff_le_discriminantExponent (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 K).integer ^ n ∣ discriminantIdeal K L ↔ n ≤ discriminantExponent K L

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

theorem TauCeti.inertiaDegree_mul_ramificationIndex_sub_one_le_discriminantExponent (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] : inertiaDegree K L * (ramificationIndex K L - 1) ≤ discriminantExponent K L

The first half of Dedekind's different theorem, for the discriminant: the discriminant exponent is at least f(L/K) · (e(L/K) - 1).

theorem TauCeti.ramificationIndex_sub_one_le_discriminantExponent (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 ≤ discriminantExponent K L

The discriminant exponent is at least e(L/K) - 1.

@[simp]

theorem TauCeti.discriminantExponent_eq_inertiaDegree_mul_ramificationIndex_sub_one_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] : discriminantExponent K L = inertiaDegree K L * (ramificationIndex K L - 1) ↔ IsTamelyRamified K L

Dedekind's different theorem for the discriminant in the tame case: δ(L/K) = f(L/K) · (e(L/K) - 1) exactly when L/K is tamely ramified.

@[simp]

theorem TauCeti.discriminantExponent_eq_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] [Algebra.IsSeparable K L] : discriminantExponent K L = 0 ↔ IsUnramified K L

The local discriminant exponent vanishes exactly for unramified extensions: δ(L/K) = 0 if and only if L/K is unramified.

@[simp]

theorem TauCeti.discriminantIdeal_eq_top_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] : discriminantIdeal K L = ⊤ ↔ IsUnramified K L

The discriminant of a local extension is trivial exactly when the extension is unramified: 𝔩(L/K) = 𝒪[K] if and only if L/K is unramified.

theorem TauCeti.discriminantIdeal_eq_of_algEquiv (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 : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K L] [Module.Finite K M] (e : L ≃ₐ[K] M) : discriminantIdeal K L = discriminantIdeal K M

The discriminant ideal is unchanged by an equivalence of extensions over the base field.

theorem TauCeti.discriminantExponent_eq_of_algEquiv (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 : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K L] [Module.Finite K M] (e : L ≃ₐ[K] M) : discriminantExponent K L = have x := ⋯; discriminantExponent K M

The local discriminant exponent is invariant under equivalence of finite extensions.