Relative norms in finite separable extensions

The relative norm formula requires separability of the particular fraction-field extension, which suffices also for function fields with imperfect base fields. This file retains the project's separable-extension interface to Mathlib's Ideal.relNorm_eq_pow_of_isMaximal and records its consequence for weighted sums of prime factors.

theorem MarkoffRiemannRoch.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] : (Ideal.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 is the project's interface to Ideal.relNorm_eq_pow_of_isMaximal.

theorem MarkoffRiemannRoch.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 ((Ideal.relNorm R) I))).sum = (Multiset.map (fun (P : Ideal S) => P.inertiaDeg R * w (Ideal.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.