Recovering an ideal from its relative norm

For a finite torsion-free extension A → B of Dedekind domains, the relative norm Ideal.relNorm A : Ideal B →*₀ Ideal A is monotone but far from injective. It is, however, injective on any chain: two nested ideals with the same relative norm are equal.

This is the step that turns a containment obtained from generators into an equality, which is how norm computations identify an ideal. Mathlib's Mathlib/RingTheory/Ideal/Norm/RelNorm.lean has the ingredients — multiplicativity, Ideal.relNorm_eq_bot_iff and Ideal.relNorm_le_comap — but not this consequence.

Main results

• Ideal.eq_of_le_of_relNorm_eq: a containment of ideals of B with equal relative norms over A is an equality.
• Ideal.dvd_relNorm_iff_exists_liesOver_dvd: a nonzero prime divides a relative norm exactly when a prime above it divides the original ideal.
• Ideal.relNorm_eq_of_forall_inertiaDeg_eq_one: over a maximal ideal p all of whose primes have inertia degree one, the relative norm of each prime above p is p itself. This is the formula N(P) = p ^ f(P ∣ p) with every f equal to 1, stated without the perfect-base-field hypothesis of Mathlib's Ideal.relNorm_eq_pow_of_isMaximal, so that it applies to extensions of function fields in positive characteristic.

theorem Ideal.eq_of_le_of_relNorm_eq {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] {I J : Ideal B} (hIJ : I ≤ J) (hnorm : (relNorm A) I = (relNorm A) J) : I = J

A containment of ideals with equal relative norms is an equality.

theorem Ideal.dvd_relNorm_iff_exists_liesOver_dvd {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] {p : Ideal A} [p.IsPrime] (hp : p ≠ ⊥) {I : Ideal B} : p ∣ (relNorm A) I ↔ ∃ (P : ↑(p.primesOver B)), ↑P ∣ I

Prime divisors of a relative norm are exactly the primes lying below prime divisors.

For a nonzero prime ideal p of A and an ideal I of B, p divides the relative norm of I if and only if some prime ideal of B lying over p divides I.

theorem Ideal.relNorm_eq_of_forall_inertiaDeg_eq_one {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] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥) (hf : ∀ Q ∈ p.primesOver B, Q.inertiaDeg A = 1) (P : Ideal B) [P.IsPrime] [P.LiesOver p] : (relNorm A) P = p

Over a maximal ideal all of whose primes have inertia degree one, the relative norm of each prime above it is that maximal ideal. This is N(P) = p ^ f(P ∣ p) when every f is 1, with no separability or Galois hypothesis on the extension.