Relative norms in finite separable extensions

The separable-extension relative-norm theorem is now available in Mathlib as Ideal.relNorm_eq_pow_of_isMaximal. This file preserves the project's original name and records the resulting weighted sum formula for prime factors.

theorem Ideal.relNorm_eq_pow_of_isMaximal_of_isSeparable {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (P : Ideal S) (p : Ideal R) [P.LiesOver p] [P.IsMaximal] [p.IsMaximal] : (relNorm R) P = p ^ P.inertiaDeg R

The relative norm of a maximal ideal in a finite separable extension is the corresponding prime below, raised to the inertia degree. This preserves the original project name for Ideal.relNorm_eq_pow_of_isMaximal.

theorem Ideal.sum_normalizedFactors_relNorm_of_isSeparable {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) (hI : I ≠ ⊥) (w : Ideal R → ℕ) : (Multiset.map w (UniqueFactorizationMonoid.normalizedFactors ((relNorm R) I))).sum = (Multiset.map (fun (P : Ideal S) => P.inertiaDeg R * w (under R P)) (UniqueFactorizationMonoid.normalizedFactors I)).sum

Relative norm preserves the weighted sum of prime factors, with each prime upstairs weighted by its inertia degree over the prime below.