English
As fractional ideals, the finite mulSupport remains finite after coercion to fractional ideals.
Русский
Как дробные идеалы, конечная поддержка сохраняется после приведения к дробному идеалу.
LaTeX
$$$(\text{mulSupport } v \mapsto (v.asIdeal)^{\text{count}(I)}).\Finite$$$
Lean4
/-- For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
`v^(val_v(I))`, regarded as a fractional ideal, is not `(1)`. -/
theorem finite_mulSupport_coe {I : Ideal R} (hI : I ≠ 0) :
(mulSupport fun v : HeightOneSpectrum R =>
(v.asIdeal : FractionalIdeal R⁰ K) ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ)).Finite :=
by
rw [mulSupport]
simp_rw [Ne, zpow_natCast, ← FractionalIdeal.coeIdeal_pow, FractionalIdeal.coeIdeal_eq_one]
exact finite_mulSupport hI
