English
For height-one spectrum v1, v2 of 𝓞 K, mk v1 = mk v2 iff v1 = v2; under certain technical assumptions, equality of evaluations implies equality of places.
Русский
Для полей v1, v2 из HeightOneSpectrum(𝓞 K) равенство mk v1 = mk v2 эквивалентно v1 = v2 (при заданных предположениях).
LaTeX
$$$\\mathrm{mk}\\,v_1 = \\mathrm{mk}\\,v_2 \\iff v_1 = v_2$$$
Lean4
@[simp]
theorem mk_eq_iff {v₁ v₂ : HeightOneSpectrum (𝓞 K)} : mk v₁ = mk v₂ ↔ v₁ = v₂ :=
by
refine ⟨?_, fun a ↦ by rw [a]⟩
contrapose!
intro h
rw [DFunLike.ne_iff]
have ⟨x, hx1, hx2⟩ : ∃ x : 𝓞 K, x ∈ v₁.asIdeal ∧ x ∉ v₂.asIdeal :=
by
by_contra! H
exact h <| HeightOneSpectrum.ext_iff.mpr <| IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H
use x
simp only [mk_apply]
rw [← norm_lt_one_iff_mem] at hx1
rw [← norm_eq_one_iff_notMem] at hx2
linarith
