feat(NumberTheory/NumberField/Completion/FinitePlace): add multiplicity lemmas (#39008)

This adds some more API for multiplicities of prime ideals in factorizations (and some more basic API lemmas, too), in preparation for a proof of the Northcott property for heights on number fields.

We also extend the API for `HasFinite{Mul|}Support` a bit.

Author: MichaelStollBayreuth

Mathlib/Algebra/FiniteSupport/Basic.lean

@@ -7,10 +7,13 @@ module
 
 public import Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
 public import Mathlib.Algebra.FiniteSupport.Defs
+public import Mathlib.Algebra.Group.Action.Pi
+public import Mathlib.Algebra.GroupWithZero.Action.Defs
 public import Mathlib.Algebra.Order.Group.Indicator
 public import Mathlib.Data.Set.Finite.Lattice
 
-import Mathlib.Algebra.Group.Support
+import Mathlib.Algebra.GroupWithZero.Indicator
+import Mathlib.Algebra.Module.Basic
 
 /-!
 # Make `fun_prop` work for finite (multiplicative) support
@@ -181,6 +184,54 @@ lemma HasFiniteMulSupport.of_comp [One β] (hfg : (f ∘ g).HasFiniteMulSupport)
   refine Set.Finite.subset hfg fun _ ha ↦ Set.mem_setOf.mpr fun H ↦ Set.mem_setOf.mp ha ?_
   grind
 
+-- The additive version is a special case of `Function.HasFiniteSupport.smul_left`.
+@[fun_prop]
+lemma HasFiniteSupport.hasFiniteMulSupport_fun_pow {M : Type*} [Monoid M] (f : α → M) {g : α → ℕ}
+    (hg : g.HasFiniteSupport) :
+    (fun a : α ↦ f a ^ g a).HasFiniteMulSupport :=
+  Set.Finite.subset hg fun a ha ↦ by contrapose! ha; simp_all
+
+section MulZeroClass
+
+variable {M : Type*} [MulZeroClass M]
+
+@[to_fun (attr := fun_prop)]
+lemma HasFiniteSupport.mul_left {f : α → M} (hf : f.HasFiniteSupport) (g : α → M) :
+    (f * g).HasFiniteSupport :=
+  Set.Finite.subset hf fun _ ha ↦ support_mul_subset_left f g ha
+
+@[to_fun (attr := fun_prop)]
+lemma HasFiniteSupport.mul_right (f : α → M) {g : α → M} (hg : g.HasFiniteSupport) :
+    (f * g).HasFiniteSupport :=
+  Set.Finite.subset hg fun _ ha ↦ support_mul_subset_right f g ha
+
+end MulZeroClass
+
 end Function
 
+@[fun_prop]
+lemma Multiset.hasFiniteSupport_count {α : Type*} [DecidableEq α] (s : Multiset α) :
+    (count · s).HasFiniteSupport :=
+  s.toFinset.finite_toSet.subset <| by simp
+
 end
+
+namespace Function.HasFiniteSupport
+
+public section SMul
+
+variable {α R M : Type*} [Zero M]
+
+@[to_fun (attr := fun_prop)]
+lemma smul_left [Zero R] [SMulWithZero R M] {f : α → R} (hf : f.HasFiniteSupport) (g : α → M) :
+    (f • g).HasFiniteSupport :=
+  Set.Finite.subset hf fun _ ha ↦ support_smul_subset_left f g ha
+
+@[to_fun (attr := fun_prop)]
+lemma smul_right [SMulZeroClass R M] (f : α → R) {g : α → M} (hg : g.HasFiniteSupport) :
+    (f • g).HasFiniteSupport :=
+  Set.Finite.subset hg fun _ ha ↦ support_smul_subset_right f g ha
+
+end SMul
+
+end Function.HasFiniteSupport

Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

@@ -352,6 +352,7 @@ theorem maximalIdeal_mk (v : HeightOneSpectrum (𝓞 K)) : maximalIdeal (mk v) =
   rw [← mk_eq_iff, mk_maximalIdeal]
 
 /-- The equivalence between finite places and maximal ideals. -/
+@[simps apply]
 noncomputable def equivHeightOneSpectrum :
     FinitePlace K ≃ HeightOneSpectrum (𝓞 K) where
   toFun := maximalIdeal
@@ -393,6 +394,13 @@ theorem hasFiniteMulSupport {x : K} (h_x_nezero : x ≠ 0) :
 
 @[deprecated (since := "2026-03-03")] alias mulSupport_finite := hasFiniteMulSupport
 
+lemma hasFiniteMulSupport_fun_pow_multiplicity {M : Type*} [CommMonoid M] {I : Ideal (𝓞 K)}
+    (hI : I ≠ ⊥) (f : Ideal (𝓞 K) → M) :
+    (fun v : FinitePlace K ↦
+      f v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I).HasFiniteMulSupport :=
+  UniqueFactorizationMonoid.hasFiniteMulSupport_fun_pow_multiplicity _
+    (asIdeal_injective.comp maximalIdeal_injective) (fun v ↦ v.maximalIdeal.irreducible) hI
+
 protected
 lemma add_le (v : FinitePlace K) (x y : K) :
     v (x + y) ≤ max (v x) (v y) := by
@@ -414,6 +422,17 @@ alias IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply :=
 @[deprecated (since := "2026-03-11")]
 alias IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm := embedding_mul_absNorm
 
+lemma finprod_finitePlace_pow_multiplicity {I : Ideal (𝓞 K)} (hI : I ≠ ⊥) :
+    ∏ᶠ v : FinitePlace K, v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I = I := by
+  conv_rhs => rw [← finprod_heightOneSpectrum_pow_multiplicity hI]
+  simp only [← finprod_comp_equiv (equivHeightOneSpectrum (K := K)), equivHeightOneSpectrum_apply]
+
+lemma apply_mul_absNorm_pow_eq_one (v : FinitePlace K) {x : 𝓞 K} (hx : x ≠ 0) :
+    v x * v.maximalIdeal.asIdeal.absNorm ^ multiplicity v.maximalIdeal.asIdeal (span {x}) = 1 := by
+  have hnz : span {x} ≠ ⊥ := mt Submodule.span_singleton_eq_bot.mp hx
+  rw [← norm_embedding_eq v x, ← Nat.cast_pow, ← map_pow, ← maxPowDividing_eq_pow_multiplicity hnz]
+  exact HeightOneSpectrum.embedding_mul_absNorm K v.maximalIdeal hx
+
 end FinitePlace
 
 section LiesOver

Mathlib/RingTheory/Algebraic/Integral.lean

@@ -192,6 +192,32 @@ theorem iff_exists_smul_integral [IsReduced R] :
   ⟨(exists_integral_multiple ·), fun ⟨_, hy, int⟩ ↦
     of_smul_isIntegral (by rwa [isNilpotent_iff_eq_zero]) int⟩
 
+section integralClosure
+
+variable {K : Type*} [CommRing K] [Algebra S K] [Algebra R K] [IsIntegralClosure S R K]
+
+variable (S)
+
+omit [Algebra R S] in
+/-- If `x : K` is algebraic over some ring `R`, then a nonzero `R`-multiple of it is contained
+in the integral closure of `R` in `K`. -/
+lemma exists_smul_eq {x : K} (hx : IsAlgebraic R x) :
+    ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = algebraMap S K s := by
+  obtain ⟨r, hr, h⟩ := hx.exists_integral_multiple
+  obtain ⟨s, hs⟩ := IsIntegralClosure.isIntegral_iff (A := S) |>.mp h
+  exact ⟨r, s, hr, hs.symm⟩
+
+/-- If `x : K` is algebraic over `ℤ`, then a nonzero `ℕ`-multiple of it is contained in the
+integral closure of `ℤ` in `K`. -/
+lemma exists_nsmul_eq [IsIntegralClosure S ℤ K] {x : K} (hx : IsAlgebraic ℤ x) :
+    ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = algebraMap S K s := by
+  obtain ⟨a, s, ha, h⟩ := hx.exists_smul_eq S
+  obtain ⟨n, rfl | rfl⟩ := a.eq_nat_or_neg
+  · exact ⟨n, s, mod_cast ha, mod_cast h⟩
+  · exact ⟨n, -s, by simpa using ha, by simp [← h]⟩
+
+end integralClosure
+
 section restrictScalars
 
 variable (R) [NoZeroDivisors S]

Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

@@ -510,6 +510,12 @@ theorem prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime
 instance : Coe (HeightOneSpectrum R) (Ideal R) where
   coe P := P.asIdeal
 
+omit [IsDedekindDomain R] in
+lemma asIdeal_injective : (HeightOneSpectrum.asIdeal (R := R)).Injective :=
+  fun ⦃_ _⦄ h ↦ HeightOneSpectrum.ext h
+
+alias asIdeal_inj := HeightOneSpectrum.ext
+
 /--
 The (nonzero) prime elements of the monoid with zero `Ideal R` correspond
 to an element of type `HeightOneSpectrum R`.

Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

@@ -9,6 +9,8 @@ public import Mathlib.Algebra.BigOperators.Finprod
 public import Mathlib.RingTheory.Multiplicity
 public import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
 
+import Mathlib.Algebra.FiniteSupport.Basic
+
 /-!
 # Unique factorization and multiplicity
 
@@ -176,4 +178,12 @@ lemma pow_dvd_pow_iff_dvd {a b : R} {n : ℕ} (hn : n ≠ 0) : a ^ n ∣ b ^ n 
   rwa [emultiplicity_pow hp, emultiplicity_pow hp,
     ENat.mul_le_mul_left_iff (by exact_mod_cast hn) (ENat.coe_ne_top _)] at this
 
+@[fun_prop]
+lemma hasFiniteMulSupport_fun_pow_multiplicity {α M : Type*} [CommMonoid M] [Subsingleton Rˣ]
+    (f : α → M) {g : α → R} (hgi : g.Injective) (hg : ∀ s, Irreducible (g s)) {r : R} (hr : r ≠ 0) :
+    (fun s : α ↦ f s ^ multiplicity (g s) r).HasFiniteMulSupport := by
+  classical
+  simp only [multiplicity_eq_count_normalizedFactors (hg _) hr, normalize_eq]
+  fun_prop
+
 end UniqueFactorizationMonoid