Dedekind's different theorem: tame and wild primes

Let B be a Dedekind domain, module-finite over a Dedekind domain A with Frac B / Frac A separable, let p be a maximal ideal of A and P a maximal ideal of B over it with ramification index e = e(P ∣ p). Mathlib's pow_sub_one_dvd_differentIdeal gives the universal half of Dedekind's different theorem, P ^ (e - 1) ∣ 𝔡(B/A). This file decides whether the next power P ^ e divides the different as well: it does exactly when P is not tame, that is, when the residue extension (B ⧸ P) / (A ⧸ p) is inseparable or the residue characteristic divides e. So the different exponent at P is exactly e - 1 at the tame primes and at least e at the others.

The criterion used is the trace criterion TauCeti.dvd_differentIdeal_iff_forall_intTrace_mem: if I * Q = p · B, then I divides 𝔡(B/A) exactly when the integral trace carries Q into p. Taking I = P ^ e and Q the prime-to-P part of p · B, the Chinese remainder theorem turns the question into whether the trace form of the A ⧸ p-algebra B ⧸ P ^ e vanishes, and Algebra.trace_quotient_pow_mk evaluates it: the trace of a residue is e times its trace in B ⧸ P. Separability of the residue extension makes the latter trace nonzero somewhere, and tameness keeps the factor e from killing it; in the wild case e is zero in A ⧸ p, and without residue separability the residue trace is zero (Algebra.trace_eq_zero_of_not_isSeparable).

Main results

• TauCeti.pow_dvd_differentIdeal_iff_of_isCoprime: the answer in the form that names a complement Q of P ^ e in p · B.
• TauCeti.pow_ramificationIdx_dvd_differentIdeal_iff: Dedekind's different theorem, second part — P ^ e(P ∣ p) ∣ 𝔡(B/A) exactly when the residue extension is inseparable or e(P ∣ p) vanishes in A ⧸ p.
• TauCeti.multiplicity_differentIdeal_eq_ramificationIdx_sub_one_iff and TauCeti.ramificationIdx_le_multiplicity_differentIdeal_iff: the multiplicity of P in the different is e(P ∣ p) - 1 exactly when the residue extension is separable and e(P ∣ p) is nonzero in A ⧸ p, and it is at least e(P ∣ p) otherwise.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.5.1(b) and Corollary 3.5.5.

theorem TauCeti.pow_dvd_differentIdeal_iff_of_isCoprime (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥) (P Q : Ideal B) [P.IsMaximal] [P.LiesOver p] {e : ℕ} (hPQ : IsCoprime (P ^ e) Q) (hmul : P ^ e * Q = Ideal.map (algebraMap A B) p) : P ^ e ∣ differentIdeal A B ↔ ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P) ∨ ↑e = 0

Dedekind's different theorem at a prime power with a coprime complement. If p · B = P ^ e * Q with P ^ e and Q coprime and p ≠ ⊥, then P ^ e divides differentIdeal A B exactly when the residue extension at P is inseparable or e vanishes in the residue field A ⧸ p.

theorem TauCeti.pow_ramificationIdx_dvd_differentIdeal_iff (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥) (P : Ideal B) [P.IsMaximal] [P.LiesOver p] : P ^ P.ramificationIdx A ∣ differentIdeal A B ↔ ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P) ∨ ↑(P.ramificationIdx A) = 0

Dedekind's different theorem, second part (Stichtenoth, Theorem 3.5.1(b) and Corollary 3.5.5): for a maximal ideal P of B over a nonzero maximal ideal p of A, the power P ^ e(P ∣ p) divides the different ideal exactly when P is not tame, that is, when the residue extension at P is inseparable or e(P ∣ p) vanishes in the residue field A ⧸ p.

Together with Mathlib's pow_sub_one_dvd_differentIdeal, the different exponent at P is therefore e(P ∣ p) - 1 at the tame primes and at least e(P ∣ p) at all others.

theorem TauCeti.ramificationIdx_le_multiplicity_differentIdeal_iff (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥) (P : Ideal B) [P.IsMaximal] [P.LiesOver p] : P.ramificationIdx A ≤ multiplicity P (differentIdeal A B) ↔ ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P) ∨ ↑(P.ramificationIdx A) = 0

Dedekind's different theorem, second part, as a bound on the exponent: the multiplicity of P in the different ideal is at least e(P ∣ p) exactly when the residue extension is inseparable or e(P ∣ p) vanishes in the residue field A ⧸ p.

theorem TauCeti.multiplicity_differentIdeal_eq_ramificationIdx_sub_one_iff (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥) (P : Ideal B) [P.IsMaximal] [P.LiesOver p] : multiplicity P (differentIdeal A B) = P.ramificationIdx A - 1 ↔ Algebra.IsSeparable (A ⧸ p) (B ⧸ P) ∧ ↑(P.ramificationIdx A) ≠ 0

Dedekind's different theorem, the tame case, as an exponent: the multiplicity of P in the different ideal is exactly e(P ∣ p) - 1 when the residue extension is separable and e(P ∣ p) is nonzero in the residue field A ⧸ p.