feat(RingTheory/Valuation): add API (leanprover-community#36110)

Prerequisites for leanprover-community#26872.

Co-authored by: @faenuccio.

Co-authored-by: mariainesdff <mariaines.dff@gmail.com>
Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>

Author: mariainesdff

Mathlib/Algebra/GroupWithZero/Range.lean

@@ -151,8 +151,15 @@ lemma restrict₀_of_ne_zero {a : A} (h : f a ≠ 0) :
     restrict₀ f a = (⟨Units.mk0 (f a) h, mem_valueGroup _ ⟨a, rfl⟩⟩ : valueGroup f) := by
   simp [h, restrict₀_apply]
 
+@[simp]
 lemma restrict₀_eq_zero_iff {a : A} : restrict₀ f a = 0 ↔ f a = 0 := by simp [restrict₀_apply]
 
+@[simp]
+lemma restrict₀_eq_one_iff {a : A} : restrict₀ f a = 1 ↔ f a = 1 := by
+  simp only [restrict₀_apply]
+  split_ifs with H <;>
+  simp [H, ← WithZero.coe_one, ← Units.mk0_one]
+
 @[simp]
 lemma embedding_restrict₀ (a : A) : ValueGroup₀.embedding (restrict₀ f a) = f a := by
   simp only [restrict₀_apply, embedding_apply]
@@ -176,7 +183,8 @@ lemma valueMonoid_eq_valueGroup : (valueMonoid f) = (valueGroup f).toSubmonoid :
     simp [hy]
   · simp [Submonoid.closure_union]
 
-variable (f) in
+variable (f)
+
 lemma valueMonoid_eq_valueGroup' : (valueMonoid f : Set Bˣ) = valueGroup f := by
   rw [valueMonoid_eq_valueGroup, coe_toSubmonoid]
 
@@ -191,6 +199,26 @@ lemma valueGroup_eq_range : Units.val '' (valueGroup f) = (range f \ {0}) := by
     refine ⟨Units.mk0 x hx₀, ?_, rfl⟩
     simpa [Units.val_mk0, mem_range] using ⟨y, hy⟩
 
+@[simp]
+lemma ValueGroup₀.restrict₀_range_eq_top : range (ValueGroup₀.restrict₀ f) = ⊤ := by
+  rw [top_eq_univ, range_eq_univ]
+  intro x
+  match x with
+  | 0 => use 0; simp
+  | some ⟨u, hu⟩ =>
+    change u ∈ (valueGroup f : Set Bˣ) at hu
+    rw [← valueMonoid_eq_valueGroup'] at hu
+    obtain ⟨v, hv⟩ := hu
+    use v
+    simp [restrict₀_apply, hv, Units.ne_zero, WithZero.coe]
+
+open Function
+
+lemma ValueGroup₀.restrict₀_surjective : Surjective (ValueGroup₀.restrict₀ f) :=
+  fun _ ↦ mem_range.mp (by simp [ValueGroup₀.restrict₀_range_eq_top])
+
+open Function
+
 end GroupWithZero
 section CommGroupWithZero
 --

Mathlib/Algebra/Order/GroupWithZero/Range.lean

@@ -38,32 +38,29 @@ lemma monoidWithZeroHom_strictMono :
     StrictMono (orderMonoidWithZeroHom f) :=
   map'_strictMono (Subtype.strictMono_coe _)
 
-variable (f) in
-/-- The inclusion of `ValueGroup₀ f` into `WithZero Bˣ` as an order embedding. In general, prefer
-the use of `MonoidWithZeroHom` and apply the above lemma
-`MonoidWithZeroHom_strictMono` if properties about ordering are needed. -/
-def orderEmbedding : ValueGroup₀ f ↪o WithZero Bˣ where
-  __ := orderMonoidWithZeroHom f
-  inj' := monoidWithZeroHom_strictMono.injective
-  map_rel_iff' := monoidWithZeroHom_strictMono.le_iff_le
-
-@[simp]
-lemma orderEmbedding_apply (x : ValueGroup₀ f) :
-    orderEmbedding f x = orderMonoidWithZeroHom f x := rfl
-
-lemma orderEmbedding_mul (x y : ValueGroup₀ f) :
-    orderEmbedding f (x * y) = orderEmbedding f x * orderEmbedding f y := by simp
+lemma embedding_strictMono : StrictMono (embedding (f := f)) := by
+  intro x y hxy
+  rw [← monoidWithZeroHom_strictMono.lt_iff_lt] at hxy
+  simpa using (OrderEmbedding.lt_iff_lt (OrderIso.withZeroUnits.toOrderEmbedding)).mpr hxy
 
 instance : IsOrderedMonoid (ValueGroup₀ f) :=
-  Function.Injective.isOrderedMonoid (orderEmbedding f) orderEmbedding_mul
-    <| OrderEmbedding.le_iff_le (orderEmbedding f)
+  Function.Injective.isOrderedMonoid embedding (map_mul _) embedding_strictMono.le_iff_le
 
 instance : LinearOrderedCommGroupWithZero (ValueGroup₀ f) where
   zero_le := by simp
   mul_lt_mul_of_pos_left a ha b c hbc := by
-    simp only [← OrderEmbedding.lt_iff_lt (orderEmbedding f), orderEmbedding_mul] at *
+    simp only [← (embedding_strictMono (f := f)).lt_iff_lt, map_mul] at *
     exact (mul_lt_mul_iff_of_pos_left ha).mpr hbc
 
+lemma embedding_unit_pos (a : (ValueGroup₀ f)ˣ) :
+    0 < embedding a.1 := by
+  conv_lhs => rw [← map_zero f, ← ValueGroup₀.embedding_restrict₀ (0 : A)]
+  rw [embedding_strictMono.lt_iff_lt]
+  simp
+
+lemma embedding_unit_ne_zero (a : (ValueGroup₀ f)ˣ) :
+    embedding a.1 ≠ 0 := (embedding_unit_pos a).ne.symm
+
 end ValueGroup₀
 
 end MonoidWithZeroHom

Mathlib/RingTheory/Valuation/Basic.lean

@@ -1,11 +1,11 @@
 /-
 Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kevin Buzzard, Johan Commelin, Patrick Massot
+Authors: Kevin Buzzard, Johan Commelin, Patrick Massot, Filippo A. E. Nuccio
 -/
 module
 
-public import Mathlib.Algebra.GroupWithZero.Range
+public import Mathlib.Algebra.Order.GroupWithZero.Range
 public import Mathlib.Algebra.Order.Hom.Monoid
 public import Mathlib.Algebra.Order.Ring.Basic
 public import Mathlib.Algebra.Ring.Torsion
@@ -453,6 +453,108 @@ lemma mem_leAddSubgroup_iff {v : Valuation R Γ₀} {γ : Γ₀} {x : R} :
 lemma leAddSubgroup_monotone (v : Valuation R Γ₀) : Monotone v.leAddSubgroup :=
   fun _ _ h _ ↦ h.trans'
 
+open MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The restriction of a valuation so that it takes values in its `valueGroup₀`. -/
+def restrict : Valuation R (MonoidWithZeroHom.ValueGroup₀ (v : R →*₀ Γ₀)) where
+  __ := restrict₀ v
+  map_add_le_max' x y := by
+    by_cases H : v x ≠ 0 ∨ v y ≠ 0
+    · rcases H with h | h <;>
+      simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, h, ↓reduceDIte] <;>
+      · split_ifs with H _ hy
+        all_goals simp [← Units.val_le_val]
+        simpa using map_add_le _ (by simp_all) (by simp_all)
+    · simp only [ne_eq, not_or, Decidable.not_not] at H
+      simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, H, ↓reduceDIte, max_self,
+        le_zero_iff, dite_eq_left_iff, WithZero.coe_ne_zero, imp_false, Decidable.not_not]
+      simpa using map_add_le _ (le_of_eq H.1) (le_of_eq H.2)
+
+lemma restrict_def (x : R) : v.restrict x = restrict₀ v x := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma restrict_pos_iff (x : R) : 0 < v.restrict x ↔ 0 < v x := by
+  simp only [restrict_def, restrict₀_apply]
+  split_ifs with h <;>
+  simp_all [zero_lt_iff.mpr]
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma restrict_lt_iff {x y : R} : v.restrict x < v.restrict y ↔ v x < v y := by
+  simp only [restrict_def, restrict₀_apply]
+  split_ifs with hx hy <;> simp_all [zero_lt_iff.mpr, ← Units.val_lt_val]
+
+set_option backward.isDefEq.respectTransparency false in
+lemma restrict_lt_iff_lt_embedding {x : R} {g : ValueGroup₀ v} :
+    v.restrict x < g ↔ v x < embedding g := by
+  conv_rhs => rw [← ValueGroup₀.embedding_restrict₀ x]
+  rw [embedding_strictMono.lt_iff_lt, restrict_def]
+
+set_option backward.isDefEq.respectTransparency false in
+lemma restrict_le_iff_le_embedding {x : R} {g : ValueGroup₀ v} :
+    v.restrict x ≤ g ↔ v x ≤ embedding g := by
+  conv_rhs => rw [← ValueGroup₀.embedding_restrict₀ x]
+  rw [embedding_strictMono.le_iff_le, restrict_def]
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma restrict_lt_one_iff {x : R} : v.restrict x < 1 ↔ v x < 1 := by
+  rw [restrict_lt_iff_lt_embedding, map_one]
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma restrict_le_one_iff {x : R} : v.restrict x ≤ 1 ↔ v x ≤ 1 := by
+  rw [restrict_le_iff_le_embedding, map_one]
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma restrict_eq_zero_iff {x : R} : v.restrict x = 0 ↔ v x = 0 := by
+  rw [restrict_def,restrict₀_eq_zero_iff]
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma restrict_eq_one_iff {x : R} : v.restrict x = 1 ↔ v x = 1 := by
+  rw [restrict_def,restrict₀_eq_one_iff]
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma restrict_le_iff {x y : R} : v.restrict x ≤ v.restrict y ↔ v x ≤ v y := by
+  simp only [restrict_def, restrict₀_apply]
+  split_ifs with hx hy <;> simp_all [← Units.val_le_val]
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma restrict_inj {x y : R} : v.restrict x = v.restrict y ↔ v x = v y := by
+  simp only [restrict_def, restrict₀_apply]
+  aesop
+
+@[simp]
+lemma embedding_restrict (x : R) : ValueGroup₀.embedding (v.restrict x) = v x :=
+  embedding_restrict₀ x
+
+set_option backward.isDefEq.respectTransparency false in
+lemma exists_div_eq_of_unit (γ : (ValueGroup₀ v)ˣ) :
+    ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = γ.1 := by
+  set u := WithZero.unzero (Units.ne_zero γ) with hu_def
+  obtain ⟨a, ⟨ha, x, hax⟩⟩ := (mem_valueGroup_iff_of_comm _).mp u.2
+  have hx : 0 < v x := by
+    rw [← restrict_pos_iff, restrict_def, WithZero.pos_iff_ne_zero, ne_eq, restrict₀_eq_zero_iff]
+    aesop
+  use x, a, hx, zero_lt_iff.mpr ha
+  have ha0 : v.restrict a ≠ 0 := by simp [ha]
+  rw [div_eq_iff ha0, mul_comm, ← embedding_strictMono.injective.eq_iff, map_mul,
+    embedding_restrict, embedding_restrict, ← hax]
+  congr
+  rw [← WithZero.coe_unzero (Units.ne_zero γ)]
+  exact Eq.refl ..
+
+lemma IsEquiv.restrict {Γ₀' : Type*} [LinearOrderedCommGroupWithZero Γ₀']
+    {w : Valuation R Γ₀'} (h : v.IsEquiv w) : v.restrict.IsEquiv w.restrict := by
+  simp only [IsEquiv] at h ⊢
+  simp [restrict_le_iff, h]
+
 /-- The subgroup of elements whose valuation is less than a certain unit. -/
 @[simps] def ltAddSubgroup (v : Valuation R Γ₀) (γ : Γ₀ˣ) : AddSubgroup R where
   carrier := { x | v x < γ }