Multiplicity after extending an ideal

The emultiplicity theorem in mathlib is the generic local factorization statement. This file records the Nat-valued wrapper used by the exact-constant genus transport, first for a specified pair of height-one places and then with the lower place chosen by under.

theorem BGS.HasseWeil.multiplicity_map_eq_ramificationIdx_mul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.IsTorsionFree R S] (v : IsDedekindDomain.HeightOneSpectrum R) (w : IsDedekindDomain.HeightOneSpectrum S) [w.asIdeal.LiesOver v.asIdeal] (I : Ideal R) (hI : I ≠ ⊥) : multiplicity w.asIdeal (Ideal.map (algebraMap R S) I) = w.asIdeal.ramificationIdx R * multiplicity v.asIdeal I

Extending a nonzero ideal multiplies its multiplicity at a height-one prime by the ramification index of that prime.

theorem BGS.HasseWeil.multiplicity_map_eq_ramificationIdx_mul_under {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra R S] [Module.IsTorsionFree R S] [Algebra.IsIntegral R S] (w : IsDedekindDomain.HeightOneSpectrum S) (I : Ideal R) (hI : I ≠ ⊥) : multiplicity w.asIdeal (Ideal.map (algebraMap R S) I) = w.asIdeal.ramificationIdx R * multiplicity (IsDedekindDomain.HeightOneSpectrum.under R w).asIdeal I

The same formula with the lower place chosen canonically by contraction.