Relative norms in finite separable extensions #
Mathlib's theorem Ideal.relNorm_eq_pow_of_isMaximal assumes that the fraction field of the
base Dedekind domain is perfect. For function fields the needed hypothesis is instead already
available in its sharp form: the particular fraction-field extension is separable. This file
records that variant, using the same normal-closure argument as the Mathlib theorem.
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]
:
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 separable-extension variant of
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) => (under R P).inertiaDeg' P * 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.