English
I is principal iff there exists x with I = { y ∈ O | v(φ(y)) ≤ v(φ(x)) }.
Русский
I является порожденным порогом тогда и только тогда, если существует x такое, что I = { y ∈ O | v(φ(y)) ≤ v(φ(x)) }.
LaTeX
$$I.IsPrincipal \iff ∃ x, I = { y ∈ O | v(\mathrm{algebraMap}(O,F)(y)) ≤ v(\mathrm{algebraMap}(O,F)(x)) }$$
Lean4
theorem isPrincipal_iff_exists_eq_setOf_valuation_le (hv : Integers v O) {I : Ideal O} :
I.IsPrincipal ↔ ∃ x, (I : Set O) = {y | v (algebraMap O F y) ≤ v (algebraMap O F x)} :=
by
rw [isPrincipal_iff_exists_isGreatest hv]
constructor <;> rintro ⟨x, hx⟩
· obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left
refine ⟨a, ?_⟩
ext b
simp only [SetLike.mem_coe, mem_setOf_eq]
constructor <;> intro h
· exact hx.right (Set.mem_image_of_mem _ h)
· rw [le_iff_dvd hv] at h
exact Ideal.mem_of_dvd I h ha
· refine ⟨v (algebraMap O F x), Set.mem_image_of_mem _ ?_, ?_⟩
· simp [hx]
· simp [hx, mem_upperBounds]
