English
If an element x ∈ K has valuation ≤ 1 at every height-one valuation, then x lies in the image of R in K.
Русский
Если элемент x ∈ K имеет valuation ≤ 1 при каждой оценке высоты единицы, тогда x лежит в образе R в K.
LaTeX
$$(∀ v, v.valuation_K(x) ≤ 1) → x ∈ (algebraMap R K).range$$
Lean4
theorem mem_integers_of_valuation_le_one (x : K) (h : ∀ v : HeightOneSpectrum R, v.valuation K x ≤ 1) :
x ∈ (algebraMap R K).range :=
by
obtain ⟨⟨n, d, hd⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors R) x
obtain rfl : x = IsLocalization.mk' K n ⟨d, hd⟩ := IsLocalization.eq_mk'_iff_mul_eq.mpr hx
obtain rfl | hn0 := eq_or_ne n 0
· simp
have hd0 := nonZeroDivisors.ne_zero hd
suffices Ideal.span { d } ∣ (Ideal.span { n } : Ideal R)
by
obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)
use z
rw [map_mul, mul_comm, mul_eq_mul_left_iff] at hx
exact (hx.resolve_right fun h => by simp [hd0] at h).symm
classical
have ine {r : R} : r ≠ 0 → Ideal.span { r } ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp
rw [← Associates.mk_le_mk_iff_dvd, ← Associates.factors_le, Associates.factors_mk _ (ine hn0),
Associates.factors_mk _ (ine hd0), WithTop.coe_le_coe, Multiset.le_iff_count]
rintro ⟨v, hv⟩
obtain ⟨v, rfl⟩ := Associates.mk_surjective v
have hv' := hv
rw [Associates.irreducible_mk, irreducible_iff_prime] at hv
specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩
simp_rw [valuation_of_mk', intValuation_if_neg _ hn0, intValuation_if_neg _ hd0, ← WithZero.coe_div, ←
WithZero.coe_one, WithZero.coe_le_coe, Associates.factors_mk _ (ine hn0), Associates.factors_mk _ (ine hd0),
Associates.count_some hv'] at h
simpa using h
