feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered

Mathlib.lean

@@ -4048,6 +4048,7 @@ import Mathlib.RingTheory.Unramified.Basic
 import Mathlib.RingTheory.Unramified.Derivations
 import Mathlib.RingTheory.Unramified.Finite
 import Mathlib.RingTheory.Valuation.AlgebraInstances
+import Mathlib.RingTheory.Valuation.Archimedean
 import Mathlib.RingTheory.Valuation.Basic
 import Mathlib.RingTheory.Valuation.ExtendToLocalization
 import Mathlib.RingTheory.Valuation.Integers

Mathlib/GroupTheory/ArchimedeanDensely.lean

@@ -201,6 +201,21 @@ lemma LinearOrderedAddCommGroup.discrete_or_denselyOrdered (G : Type*)
     · simp [hz.left]
     · simpa [lt_sub_iff_add_lt'] using hz.right
 
+/-- Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic)
+to the integers, or is densely ordered, exclusively. -/
+lemma LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered (G : Type*)
+    [LinearOrderedAddCommGroup G] [Archimedean G] :
+    Nonempty (G ≃+o ℤ) ↔ ¬ DenselyOrdered G := by
+  suffices ∀ (_ : G ≃+o ℤ), ¬ DenselyOrdered G by
+    rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩|h
+    · simpa [this h] using ⟨h⟩
+    · simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]
+      exact ⟨fun H ↦ (this H) h⟩
+  intro e H
+  rw [denselyOrdered_iff_of_orderIsoClass e] at H
+  obtain ⟨_, _⟩ := exists_between (one_pos (α := ℤ))
+  linarith
+
 variable (G) in
 /-- Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic)
 to the multiplicative integers, or is densely ordered. -/
@@ -211,35 +226,84 @@ lemma LinearOrderedCommGroup.discrete_or_denselyOrdered :
   rintro ⟨f, hf⟩
   exact ⟨AddEquiv.toMultiplicative' f, hf⟩
 
-/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
-either isomorphic (and order-isomorphic) to `ℤₘ₀`, or is densely ordered. -/
-lemma LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered (G : Type*)
-    [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] :
-    Nonempty (G ≃*o ℤₘ₀) ∨ DenselyOrdered G := by
-  classical
-  refine (LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp ?_ ?_
-  · intro ⟨f⟩
-    refine ⟨OrderMonoidIso.trans
-      ⟨WithZero.withZeroUnitsEquiv.symm, ?_⟩ ⟨f.withZero, ?_⟩⟩
-    · intro
-      simp only [WithZero.withZeroUnitsEquiv, MulEquiv.symm_mk,
-        MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, MulEquiv.coe_mk,
-        Equiv.coe_fn_symm_mk ]
-      split_ifs <;>
-      simp_all [← Units.val_le_val]
-    · intro a b
-      induction a <;> induction b <;>
-      simp [MulEquiv.withZero]
+variable (G) in
+/-- Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic)
+to the multiplicative integers, or is densely ordered, exclusively. -/
+@[to_additive existing]
+lemma LinearOrderedCommGroup.discrete_iff_not_denselyOrdered :
+    Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬ DenselyOrdered G := by
+  let e : G ≃o Additive G := OrderIso.refl G
+  rw [denselyOrdered_iff_of_orderIsoClass e,
+    ← LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered (Additive G)]
+  refine Nonempty.congr ?_ ?_ <;> intro f
+  · exact ⟨MulEquiv.toAdditive' f, by simp⟩
+  · exact ⟨MulEquiv.toAdditive'.symm f, by simp⟩
+
+lemma denselyOrdered_units_iff {G₀ : Type*} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] :
+    DenselyOrdered G₀ˣ ↔ DenselyOrdered G₀ := by
+  constructor
   · intro H
     refine ⟨fun x y h ↦ ?_⟩
     rcases (zero_le' (a := x)).eq_or_lt with rfl|hx
-    · lift y to Gˣ using h.ne'.isUnit
-      obtain ⟨z, hz⟩ := exists_ne (1 : Gˣ)
-      refine ⟨(y * |z|ₘ⁻¹ : Gˣ), ?_, ?_⟩
+    · lift y to G₀ˣ using h.ne'.isUnit
+      obtain ⟨z, hz⟩ := exists_ne (1 : G₀ˣ)
+      refine ⟨(y * |z|ₘ⁻¹ : G₀ˣ), ?_, ?_⟩
       · simp [zero_lt_iff]
       · rw [Units.val_lt_val]
         simp [hz]
     · obtain ⟨z, hz, hz'⟩ := H.dense (Units.mk0 x hx.ne') (Units.mk0 y (hx.trans h).ne')
         (by simp [← Units.val_lt_val, h])
       refine ⟨z, ?_, ?_⟩ <;>
       simpa [← Units.val_lt_val]
+  · intro H
+    refine ⟨fun x y h ↦ ?_⟩
+    obtain ⟨z, hz⟩ := exists_between (Units.val_lt_val.mpr h)
+    rcases (zero_le' (a := z)).eq_or_lt with rfl|hz'
+    · simp at hz
+    refine ⟨Units.mk0 z hz'.ne', ?_⟩
+    simp [← Units.val_lt_val, hz]
+
+/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
+either isomorphic (and order-isomorphic) to `ℤₘ₀`, or is densely ordered. -/
+lemma LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered (G : Type*)
+    [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] :
+    Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered G := by
+  classical
+  rw [← denselyOrdered_units_iff]
+  refine (LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp_left ?_
+  intro ⟨f⟩
+  refine ⟨OrderMonoidIso.trans
+    ⟨WithZero.withZeroUnitsEquiv.symm, ?_⟩ ⟨f.withZero, ?_⟩⟩
+  · intro
+    simp only [WithZero.withZeroUnitsEquiv, MulEquiv.symm_mk,
+      MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, MulEquiv.coe_mk,
+      Equiv.coe_fn_symm_mk ]
+    split_ifs <;>
+    simp_all [← Units.val_le_val]
+  · intro a b
+    induction a <;> induction b <;>
+    simp [MulEquiv.withZero]
+
+open WithZero in
+/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
+either isomorphic (and order-isomorphic) to `ℤₘ₀`, or is densely ordered, exclusively -/
+lemma LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered (G : Type*)
+    [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] :
+    Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ↔ ¬ DenselyOrdered G := by
+  rw [← denselyOrdered_units_iff,
+      ← LinearOrderedCommGroup.discrete_iff_not_denselyOrdered]
+  refine Nonempty.congr ?_ ?_ <;> intro f
+  · refine ⟨MulEquiv.unzero (withZeroUnitsEquiv.trans f), ?_⟩
+    intros
+    simp only [MulEquiv.unzero, withZeroUnitsEquiv, MulEquiv.trans_apply,
+      MulEquiv.coe_mk, Equiv.coe_fn_mk, recZeroCoe_coe, OrderMonoidIso.coe_mulEquiv,
+      MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, map_eq_zero, coe_ne_zero,
+      ↓reduceDIte, unzero_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]
+    rw [← Units.val_le_val, ← map_le_map_iff f, ← coe_le_coe, coe_unzero, coe_unzero]
+  · refine ⟨withZeroUnitsEquiv.symm.trans (MulEquiv.withZero f), ?_⟩
+    intros
+    simp only [withZeroUnitsEquiv, MulEquiv.symm_mk, MulEquiv.withZero,
+      MulEquiv.toMonoidHom_eq_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
+      MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]
+    split_ifs <;>
+    simp_all [← Units.val_le_val]

Mathlib/Order/Hom/Basic.lean

@@ -522,6 +522,11 @@ protected def withTopMap (f : α →o β) : WithTop α →o WithTop β :=
 
 end OrderHom
 
+-- See note [lower instance priority]
+instance (priority := 100) OrderHomClass.toOrderHomClassOrderDual [LE α] [LE β]
+    [FunLike F α β] [OrderHomClass F α β] : OrderHomClass F αᵒᵈ βᵒᵈ where
+  map_rel f := map_rel f
+
 /-- Embeddings of partial orders that preserve `<` also preserve `≤`. -/
 def RelEmbedding.orderEmbeddingOfLTEmbedding [PartialOrder α] [PartialOrder β]
     (f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)) : α ↪o β :=
@@ -1272,6 +1277,11 @@ end BoundedOrder
 
 end LatticeIsos
 
+-- See note [lower instance priority]
+instance (priority := 100) OrderIsoClass.toOrderIsoClassOrderDual [LE α] [LE β]
+    [EquivLike F α β] [OrderIsoClass F α β] : OrderIsoClass F αᵒᵈ βᵒᵈ where
+  map_le_map_iff f := map_le_map_iff f
+
 section DenselyOrdered
 
 lemma denselyOrdered_iff_of_orderIsoClass {X Y F : Type*} [Preorder X] [Preorder Y]

Mathlib/Order/SuccPred/Archimedean.lean

@@ -219,6 +219,39 @@ lemma SuccOrder.forall_ne_bot_iff
   simp only [Function.iterate_succ', Function.comp_apply]
   apply h
 
+section IsLeast
+
+-- TODO: generalize to PartialOrder and `DirectedOn` after #16272
+lemma BddAbove.exists_isGreatest_of_nonempty {X : Type*} [LinearOrder X] [SuccOrder X]
+    [IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
+    ∃ x, IsGreatest S x := by
+  obtain ⟨m, hm⟩ := hS
+  obtain ⟨n, hn⟩ := hS'
+  by_cases hm' : m ∈ S
+  · exact ⟨_, hm', hm⟩
+  have hn' := hm hn
+  revert hn hm hm'
+  refine Succ.rec ?_ ?_ hn'
+  · simp (config := {contextual := true})
+  intro m _ IH hm hn hm'
+  rw [mem_upperBounds] at IH hm
+  simp_rw [Order.le_succ_iff_eq_or_le] at hm
+  replace hm : ∀ x ∈ S, x ≤ m := by
+    intro x hx
+    refine (hm x hx).resolve_left ?_
+    rintro rfl
+    exact hm' hx
+  by_cases hmS : m ∈ S
+  · exact ⟨m, hmS, hm⟩
+  · exact IH hm hn hmS
+
+lemma BddBelow.exists_isLeast_of_nonempty {X : Type*} [LinearOrder X] [PredOrder X]
+    [IsPredArchimedean X] {S : Set X} (hS : BddBelow S) (hS' : S.Nonempty) :
+    ∃ x, IsLeast S x :=
+  BddAbove.exists_isGreatest_of_nonempty (X := Xᵒᵈ) hS hS'
+
+end IsLeast
+
 section OrderIso
 
 variable {X Y : Type*} [PartialOrder X] [PartialOrder Y]

Mathlib/RingTheory/Valuation/Archimedean.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2024 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.Algebra.Order.Archimedean.Submonoid
+import Mathlib.Algebra.Order.Monoid.Submonoid
+import Mathlib.Algebra.Order.SuccPred.TypeTags
+import Mathlib.Data.Int.SuccPred
+import Mathlib.GroupTheory.ArchimedeanDensely
+import Mathlib.RingTheory.Valuation.Integers
+
+/-!
+# Ring of integers under a given valuation in an multiplicatively archimedean codomain
+
+-/
+
+namespace Valuation.Integers
+
+section Field
+
+variable {F Γ₀ O : Type*} [Field F] [LinearOrderedCommGroupWithZero Γ₀]
+  [CommRing O] [Algebra O F] {v : Valuation F Γ₀}
+
+lemma isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean Γ₀] (hv : Integers v O) :
+    IsPrincipalIdealRing O ↔ ¬ DenselyOrdered (Set.range v) := by
+  refine ⟨fun _ ↦ not_denselyOrdered_of_isPrincipalIdealRing hv, fun H ↦ ?_⟩
+  let l : LinearOrderedCommGroupWithZero (MonoidHom.mrange v) :=
+  { zero := ⟨0, by simp⟩
+    zero_mul := by
+      intro a
+      exact Subtype.ext (zero_mul a.val)
+    mul_zero := by
+      intro a
+      exact Subtype.ext (mul_zero a.val)
+    zero_le_one := Subtype.coe_le_coe.mp (zero_le_one)
+    inv := fun x ↦ ⟨x⁻¹, by
+      obtain ⟨y, hy⟩ := x.prop
+      simp_rw [← hy, ← v.map_inv]
+      exact MonoidHom.mem_mrange.mpr ⟨_, rfl⟩⟩
+    exists_pair_ne := ⟨⟨v 0, by simp⟩, ⟨v 1, by simp [- _root_.map_one]⟩, by simp⟩
+    inv_zero := Subtype.ext inv_zero
+    mul_inv_cancel := by
+      rintro ⟨a, ha⟩ h
+      simp only [ne_eq, Subtype.ext_iff] at h
+      simpa using mul_inv_cancel₀ h }
+  have h0 : (0 : MonoidHom.mrange v) = ⟨0, by simp⟩ := rfl
+  rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs|_
+  · have : ∀ x : (MonoidHom.mrange v)ˣ, x.val = 1 := by
+      intro x
+      rw [← Units.val_one, Units.eq_iff]
+      exact Subsingleton.elim _ _
+    replace this : ∀ x ≠ 0, v x = 1 := by
+      intros x hx
+      specialize this (Units.mk0 ⟨v x, by simp⟩ _)
+      · simp [ne_eq, Subtype.ext_iff, h0, hx]
+      simpa [Subtype.ext_iff] using this
+    suffices ∀ I : Ideal O, I = ⊥ ∨ I = ⊤ by
+      constructor
+      intro I
+      rcases this I with rfl|rfl
+      · exact ⟨0, Ideal.span_zero.symm⟩
+      · exact ⟨1, Ideal.span_one.symm⟩
+    intro I
+    rcases eq_or_ne I ⊤ with rfl|hI
+    · simp
+    simp only [hI, or_false]
+    ext x
+    rcases eq_or_ne x 0 with rfl|hx
+    · simp
+    · specialize this (algebraMap O F x) (by simp [map_eq_zero_iff _ hv.hom_inj, hx])
+      simp only [Ideal.mem_bot, hx, iff_false]
+      contrapose! hI
+      exact Ideal.eq_top_of_isUnit_mem _ hI (isUnit_of_one' hv this)
+  replace H : ¬ DenselyOrdered (MonoidHom.mrange v) := H
+  rw [← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered (MonoidHom.mrange v)] at H
+  obtain ⟨e⟩ := H
+  constructor
+  intro S
+  rw [isPrincipal_iff_exists_isGreatest hv]
+  rcases eq_or_ne S ⊥ with rfl|hS
+  · simp only [Function.comp_apply, Submodule.bot_coe, Set.image_singleton, _root_.map_zero]
+    exact ⟨0, by simp⟩
+  let e' : (MonoidHom.mrange v)ˣ ≃o Multiplicative ℤ := ⟨
+    (MulEquiv.unzero (WithZero.withZeroUnitsEquiv.trans e)).toEquiv, by
+    intros
+    simp only [MulEquiv.unzero, WithZero.withZeroUnitsEquiv,
+      MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_mk, WithZero.recZeroCoe_coe,
+      OrderMonoidIso.coe_mulEquiv, MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Units.val_mk0,
+      Equiv.coe_fn_symm_mk, map_eq_zero, WithZero.coe_ne_zero, ↓reduceDIte, WithZero.unzero_coe,
+      MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, ← Units.val_le_val]
+    rw [← map_le_map_iff e, ← WithZero.coe_le_coe, WithZero.coe_unzero, WithZero.coe_unzero]⟩
+  let _ : SuccOrder (MonoidHom.mrange v)ˣ := .ofOrderIso e'.symm
+  have : IsSuccArchimedean (MonoidHom.mrange v)ˣ := .of_orderIso e'.symm
+  set T : Set (MonoidHom.mrange v)ˣ := {y | ∃ (x : O) (h : x ≠ 0), x ∈ S ∧
+      y = Units.mk0 ⟨v (algebraMap O F x), by simp⟩
+      (by simp [map_ne_zero_iff, Subtype.ext_iff, h0, map_eq_zero_iff _ hv.hom_inj, h])} with hT
+  have : BddAbove (α := (MonoidHom.mrange v)ˣ) T := by
+    refine ⟨1, ?_⟩
+    simp only [ne_eq, exists_and_left, mem_upperBounds, Set.mem_setOf_eq, forall_exists_index,
+      and_imp, hT]
+    rintro _ x _ hx' rfl
+    simp [← Units.val_le_val, ← Subtype.coe_le_coe, hv.map_le_one]
+  have hTn : T.Nonempty := by
+    rw [Submodule.ne_bot_iff] at hS
+    obtain ⟨x, hx, hx'⟩ := hS
+    refine ⟨Units.mk0 ⟨v (algebraMap O F x), by simp⟩ ?_, ?_⟩
+    · simp [map_ne_zero_iff, Subtype.ext_iff, h0, map_eq_zero_iff _ hv.hom_inj, hx']
+    · simp only [hT, ne_eq, exists_and_left, Set.mem_setOf_eq, Units.mk0_inj, Subtype.mk.injEq,
+      exists_prop', nonempty_prop]
+      exact ⟨_, hx, hx', rfl⟩
+  obtain ⟨_, ⟨x, hx, hxS, rfl⟩, hx'⟩ := this.exists_isGreatest_of_nonempty hTn
+  refine ⟨_, ⟨x, hxS, rfl⟩, ?_⟩
+  simp only [hT, ne_eq, exists_and_left, mem_upperBounds, Set.mem_setOf_eq, ← Units.val_le_val,
+    Units.val_mk0, ← Subtype.coe_le_coe, forall_exists_index, and_imp, Function.comp_apply,
+    Set.mem_image, SetLike.mem_coe, forall_apply_eq_imp_iff₂] at hx' ⊢
+  intro y hy
+  rcases eq_or_ne y 0 with rfl|hy'
+  · simp
+  specialize hx' _ y hy hy' rfl
+  simpa [← Units.val_le_val, ← Subtype.coe_le_coe] using hx'
+
+end Field
+
+end Valuation.Integers