Coefficients of a relative norm

For a finite torsion-free extension A → B of Dedekind domains and a nonzero maximal ideal p of A, the coefficient of Ideal.relNorm A I at p is determined by the coefficients of I at the primes of B above p, each weighted by a residue degree:

mult_p(relNorm A I) = Σ_{P ∣ p} f(P / p) · mult_P(I).

The weights are Mathlib's: Ideal.relNorm P = p ^ f(P / p) for a maximal P above p.

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_relNorm: the coefficient of a relative norm at p is the weighted sum of the coefficients of the ideal at the primes above p.

References

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

theorem TauCeti.multiplicity_relNorm {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 ≠ ⊥) {I : Ideal B} (hI : I ≠ ⊥) : multiplicity p ((Ideal.relNorm A) I) = ∑ P ∈ (p.primesOver B).toFinset, P.inertiaDeg A * multiplicity P I

The coefficients of a relative norm. For a nonzero ideal I of B and a nonzero maximal ideal p of A, the coefficient of relNorm A I at p is the sum, over the primes P of B above p, of the coefficient of I at P weighted by the residue degree of P over p.