English
For a nonzero ideal I, the mulSupport of the associated maxPowDividing I is finite.
Русский
Для ненулевого идеала I mulSupport maxPowDividing I конечна.
LaTeX
$$$\text{mulSupport }( v.maxPowDividing I) \text{ finite}$$$
Lean4
/-- For every nonzero ideal `I` of `v`, `v^(val_v(I) + 1)` does not divide `∏_v v^(val_v(I))`. -/
theorem finprod_not_dvd (I : Ideal R) (hI : I ≠ 0) :
¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
∏ᶠ v : HeightOneSpectrum R, v.maxPowDividing I :=
by
have hf := finite_mulSupport hI
have h_ne_zero : v.maxPowDividing I ≠ 0 := pow_ne_zero _ v.ne_bot
rw [← mul_finprod_cond_ne v hf, pow_add, pow_one, finprod_cond_ne _ _ hf]
intro h_contr
have hv_prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime
obtain ⟨w, hw, hvw'⟩ := Prime.exists_mem_finset_dvd hv_prime ((mul_dvd_mul_iff_left h_ne_zero).mp h_contr)
have hw_prime : Prime w.asIdeal := Ideal.prime_of_isPrime w.ne_bot w.isPrime
have hvw := Prime.dvd_of_dvd_pow hv_prime hvw'
rw [Prime.dvd_prime_iff_associated hv_prime hw_prime, associated_iff_eq] at hvw
exact (Finset.mem_erase.mp hw).1 (HeightOneSpectrum.ext hvw.symm)
