Coefficients of the relative discriminant

The relative discriminant relDiscr A B is the relative norm of the different ideal, so its coefficient at a nonzero maximal ideal p of A is determined by the coefficients of the different at the primes of B above p, each weighted by a residue degree:

mult_p(relDiscr A B) = Σ_{P ∣ p} f(P / p) · mult_P(𝔇(B / A)).

This is the coefficient formula for relDiscr specifically: it is TauCeti.multiplicity_relNorm applied to the different, through relDiscr_def. The hypotheses are that p is a nonzero maximal ideal of A and that the different is nonzero, the latter holding whenever the extension is separable.

The coefficient mult_p(I) is Mathlib's multiplicity, the normalization in which Ideal.finprod_heightOneSpectrum_pow_multiplicity recovers an ideal from its coefficients.

Main results

• TauCeti.multiplicity_relDiscr: the coefficient of the relative discriminant at p is the weighted sum of the coefficients of the different at the primes above p.

References

• [J. Neukirch, Algebraic number theory][Neukirch1992], Chapter III, §2.

theorem TauCeti.multiplicity_relDiscr {A : Type u_1} (B : Type u_2) [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] [PerfectField (FractionRing A)] (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥) (hd : differentIdeal A B ≠ ⊥) : multiplicity p (relDiscr A B) = ∑ P ∈ (p.primesOver B).toFinset, P.inertiaDeg A * multiplicity P (differentIdeal A B)

The coefficients of the relative discriminant. At a nonzero maximal ideal p of A, the coefficient of relDiscr A B is the sum of the coefficients of the different at the primes above p, each weighted by its residue degree.