English
For I ≠ 0 represented as I = spanSingleton(a)⁻¹ · J, there exists a finite set of height-one primes outside of which the difference between the J-factors and the span(a) factors vanishes.
Русский
Для I ≠ 0, представимого как I = spanSingleton(a)⁻¹ · J, существует конечное множество высот-прайм, вне которого разность между факторами J и факторами span(a) равна нулю.
LaTeX
$$$\exists F \subseteq \mathrm{HeightOneSpectrum}(R)$ finite,\; \forall v \notin F:\; (\text{factors}(J) - \text{factors}(\mathrm{span}\{a\}) )_v = 0.$$$
Lean4
/-- If `I ≠ 0`, then `val_v(I) = 0` for all but finitely many maximal ideals of `R`. -/
theorem finite_factors' {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R} {J : Ideal R}
(haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) :
∀ᶠ v : HeightOneSpectrum R in Filter.cofinite,
((Associates.mk v.asIdeal).count (Associates.mk J).factors : ℤ) -
(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { a })).factors =
0 :=
by
have ha_ne_zero : Ideal.span { a } ≠ 0 := constant_factor_ne_zero hI haJ
have hJ_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI haJ
have h_subset :
{v : HeightOneSpectrum R |
¬((Associates.mk v.asIdeal).count (Associates.mk J).factors : ℤ) -
↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { a })).factors) =
0} ⊆
{v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span { a }} :=
by
intro v hv
have hv_irred : Irreducible v.asIdeal := v.irreducible
by_contra h_notMem
rw [mem_union, mem_setOf_eq, mem_setOf_eq] at h_notMem
push_neg at h_notMem
rw [← Associates.count_ne_zero_iff_dvd ha_ne_zero hv_irred, not_not, ←
Associates.count_ne_zero_iff_dvd hJ_ne_zero hv_irred, not_not] at h_notMem
rw [mem_setOf_eq, h_notMem.1, h_notMem.2, sub_self] at hv
exact hv (Eq.refl 0)
exact
Finite.subset
(Finite.union (Ideal.finite_factors (ideal_factor_ne_zero hI haJ))
(Ideal.finite_factors (constant_factor_ne_zero hI haJ)))
h_subset
