feat(RingTheory): Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing (#15939)

On the way to the iff when the range of valuation on nonzeros is `MulArchimedean`.




Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author: pechersky

Mathlib/RingTheory/Ideal/Basic.lean

@@ -490,6 +490,9 @@ theorem mul_mem_right (h : a ∈ I) : a * b ∈ I :=
 
 variable {b}
 
+lemma mem_of_dvd (hab : a ∣ b) (ha : a ∈ I) : b ∈ I := by
+  obtain ⟨c, rfl⟩ := hab; exact I.mul_mem_right _ ha
+
 theorem pow_mem_of_mem (ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I :=
   Nat.casesOn n (Not.elim (by decide))
     (fun m _hm => (pow_succ a m).symm ▸ I.mul_mem_left (a ^ m) ha) hn

Mathlib/RingTheory/Valuation/Integers.lean

@@ -13,6 +13,7 @@ The elements with valuation less than or equal to 1.
 TODO: Define characteristic predicate.
 -/
 
+open Set
 
 universe u v w
 
@@ -144,6 +145,50 @@ theorem eq_algebraMap_or_inv_eq_algebraMap (hv : Integers v O) (x : F) :
   obtain ⟨a, ha⟩ := exists_of_le_one hv h
   exacts [⟨a, Or.inl ha.symm⟩, ⟨a, Or.inr ha.symm⟩]
 
+lemma isPrincipal_iff_exists_isGreatest (hv : Integers v O) {I : Ideal O} :
+    I.IsPrincipal ↔ ∃ x, IsGreatest (v ∘ algebraMap O F '' I) x := by
+  constructor <;> rintro ⟨x, hx⟩
+  · refine ⟨(v ∘ algebraMap O F) x, ?_, ?_⟩
+    · refine Set.mem_image_of_mem _ ?_
+      simp [hx, Ideal.mem_span_singleton_self]
+    · intro y hy
+      simp only [Function.comp_apply, hx, Ideal.submodule_span_eq, Set.mem_image,
+        SetLike.mem_coe, Ideal.mem_span_singleton] at hy
+      obtain ⟨y, hy, rfl⟩ := hy
+      exact le_of_dvd hv hy
+  · obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left
+    refine ⟨a, ?_⟩
+    ext b
+    simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton]
+    exact ⟨fun hb ↦ dvd_of_le hv (hx.2 <| mem_image_of_mem _ hb), fun hb ↦ I.mem_of_dvd hb ha⟩
+
+lemma not_denselyOrdered_of_isPrincipalIdealRing [IsPrincipalIdealRing O] (hv : Integers v O) :
+    ¬ DenselyOrdered (range v) := by
+  intro H
+  -- nonunits as an ideal isn't defined here, nor shown to be equivalent to `v x < 1`
+  set I : Ideal O := {
+    carrier := v ∘ algebraMap O F ⁻¹' Iio (1 : Γ₀)
+    add_mem' := fun {a b} ha hb ↦ by simpa using map_add_lt v ha hb
+    zero_mem' := by simp
+    smul_mem' := by
+      intro c x
+      simp only [mem_preimage, Function.comp_apply, mem_Iio, smul_eq_mul, _root_.map_mul]
+      intro hx
+      exact Right.mul_lt_one_of_le_of_lt (hv.map_le_one c) hx
+  }
+  obtain ⟨x, hx₁, hx⟩ :
+    ∃ x, v (algebraMap O F x) < 1 ∧
+      v (algebraMap O F x) ∈ upperBounds (Iio 1 ∩ range (v ∘ algebraMap O F)) := by
+    simpa [I, IsGreatest, hv.isPrincipal_iff_exists_isGreatest, ← image_preimage_eq_inter_range]
+      using IsPrincipalIdealRing.principal I
+  obtain ⟨y, hy, hy₁⟩ : ∃ y, v (algebraMap O F x) < v y ∧ v y < 1 := by
+    simpa only [Subtype.exists, Subtype.mk_lt_mk, exists_range_iff, exists_prop]
+      using H.dense ⟨v (algebraMap O F x), mem_range_self _⟩ ⟨1, 1, v.map_one⟩ hx₁
+  obtain ⟨z, rfl⟩ := hv.exists_of_le_one hy₁.le
+  exact hy.not_le <| hx ⟨hy₁, mem_range_self _⟩
+
+-- TODO: isPrincipalIdealRing_iff_not_denselyOrdered when MulArchimedean
+
 end Integers
 
 end Field