finite_mulSupport — Mathlib

English

For a nonzero I, the support of v.maxPowDividing I over v is finite.

Русский

Для ненулевого I поддержка v.maxPowDividing I по v конечна.

LaTeX

$$$\operatorname{mulSupport}(\lambda v. v.maxPowDividing I)\text{ is finite}$$$

Lean4

/-- For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
  `v^(val_v(I))` is not the unit ideal. -/
theorem finite_mulSupport {I : Ideal R} (hI : I ≠ 0) :
    (mulSupport fun v : HeightOneSpectrum R => v.maxPowDividing I).Finite :=
  haveI h_subset :
    {v : HeightOneSpectrum R | v.maxPowDividing I ≠ 1} ⊆
      {v : HeightOneSpectrum R | ((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ) ≠ 0} :=
    by
    intro v hv h_zero
    have hv' : v.maxPowDividing I = 1 := by
      rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.natCast_eq_zero.mp h_zero, pow_zero _]
    exact hv hv'
  Finite.subset (Filter.eventually_cofinite.mp (Associates.finite_factors hI)) h_subset

Похожие утверждения