feat(Valuation/RankOne): equivalence with ValuativeRel.isRankLeOne (#26754)

refactor to have Valuation.RankOne extend the new Valuation.IsNontrivial and characterization iffs for ValuativeRel.IsNontrivial relating to units of value group, or Valuation.IsNontrivial

Author: pechersky

Mathlib/NumberTheory/NumberField/FinitePlaces.lean

@@ -104,7 +104,7 @@ noncomputable instance instRankOneValuedAdicCompletion :
     map_mul' := MonoidWithZeroHom.map_mul (toNNReal (absNorm_ne_zero v))
   }
   strictMono' := toNNReal_strictMono (one_lt_absNorm_nnreal v)
-  nontrivial' := by
+  exists_val_nontrivial := by
     rcases Submodule.exists_mem_ne_zero_of_ne_bot v.ne_bot with ⟨x, hx1, hx2⟩
     use x
     dsimp [adicCompletion]

Mathlib/NumberTheory/Padics/Complex.lean

@@ -95,7 +95,7 @@ theorem valuation_p (p : ℕ) [Fact p.Prime] : Valued.v (p : PadicAlgCl p) = 1 /
 instance : RankOne (PadicAlgCl.valued p).v where
   hom         := MonoidWithZeroHom.id ℝ≥0
   strictMono' := strictMono_id
-  nontrivial' := by
+  exists_val_nontrivial := by
     use p
     have hp : Nat.Prime p := hp.1
     simp only [valuation_p, one_div, ne_eq, inv_eq_zero, Nat.cast_eq_zero, inv_eq_one,
@@ -152,7 +152,7 @@ theorem valuation_p : Valued.v (p : ℂ_[p]) = 1 / (p : ℝ≥0) := by
 instance : RankOne (PadicComplex.valued p).v where
   hom         := MonoidWithZeroHom.id ℝ≥0
   strictMono' := strictMono_id
-  nontrivial' := by
+  exists_val_nontrivial := by
     use p
     have hp : Nat.Prime p := hp.1
     simp only [valuation_p, one_div, ne_eq, inv_eq_zero, Nat.cast_eq_zero, inv_eq_one,

Mathlib/RingTheory/Valuation/RankOne.lean

@@ -3,8 +3,7 @@ Copyright (c) 2024 María Inés de Frutos-Fernández. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: María Inés de Frutos-Fernández
 -/
-import Mathlib.Data.NNReal.Defs
-import Mathlib.RingTheory.Valuation.Basic
+import Mathlib.RingTheory.Valuation.ValuativeRel
 
 /-!
 # Rank one valuations
@@ -32,19 +31,18 @@ namespace Valuation
 
 /-- A valuation has rank one if it is nontrivial and its image is contained in `ℝ≥0`.
   Note that this class includes the data of an inclusion morphism `Γ₀ → ℝ≥0`. -/
-class RankOne (v : Valuation R Γ₀) where
+class RankOne (v : Valuation R Γ₀) extends Valuation.IsNontrivial v where
   /-- The inclusion morphism from `Γ₀` to `ℝ≥0`. -/
   hom : Γ₀ →*₀ ℝ≥0
   strictMono' : StrictMono hom
-  nontrivial' : ∃ r : R, v r ≠ 0 ∧ v r ≠ 1
 
 namespace RankOne
 
 variable (v : Valuation R Γ₀) [RankOne v]
 
 lemma strictMono : StrictMono (hom v) := strictMono'
 
-lemma nontrivial : ∃ r : R, v r ≠ 0 ∧ v r ≠ 1 := nontrivial'
+lemma nontrivial : ∃ r : R, v r ≠ 0 ∧ v r ≠ 1 := IsNontrivial.exists_val_nontrivial
 
 /-- If `v` is a rank one valuation and `x : Γ₀` has image `0` under `RankOne.hom v`, then
   `x = 0`. -/
@@ -74,3 +72,37 @@ instance [RankOne v] : IsNontrivial v where
 end RankOne
 
 end Valuation
+
+section ValuativeRel
+
+open ValuativeRel
+
+variable {R : Type*} [CommRing R] [ValuativeRel R]
+
+/-- A valuative relation has a rank one valuation when it is both nontrivial
+and the rank is at most one. -/
+def Valuation.RankOne.ofRankLeOneStruct [ValuativeRel.IsNontrivial R] (e : RankLeOneStruct R) :
+    Valuation.RankOne (valuation R) where
+  __ : Valuation.IsNontrivial (valuation R) := isNontrivial_iff_isNontrivial.mp inferInstance
+  hom := e.emb
+  strictMono' := e.strictMono
+
+instance [IsNontrivial R] [IsRankLeOne R] :
+    Valuation.RankOne (valuation R) :=
+  Valuation.RankOne.ofRankLeOneStruct IsRankLeOne.nonempty.some
+
+/-- Convert between the rank one statement on valuative relation's induced valuation. -/
+def Valuation.RankOne.rankLeOneStruct (e : Valuation.RankOne (valuation R)) :
+    RankLeOneStruct R where
+  emb := e.hom
+  strictMono := e.strictMono
+
+lemma ValuativeRel.isRankLeOne_of_rankOne [h : (valuation R).RankOne] :
+    IsRankLeOne R :=
+  ⟨⟨h.rankLeOneStruct⟩⟩
+
+lemma ValuativeRel.isNontrivial_of_rankOne [h : (valuation R).RankOne] :
+    ValuativeRel.IsNontrivial R :=
+  isNontrivial_iff_isNontrivial.mpr h.toIsNontrivial
+
+end ValuativeRel

Mathlib/RingTheory/Valuation/ValuativeRel.lean

@@ -75,7 +75,8 @@ class ValuativeRel (R : Type*) [CommRing R] where
   rel_mul_cancel {x y z} : ¬ rel z 0 → rel (x * z) (y * z) → rel x y
   not_rel_one_zero : ¬ rel 1 0
 
-@[inherit_doc] infix:50  " ≤ᵥ " => ValuativeRel.rel
+@[inherit_doc ValuativeRel.rel]
+notation:50 (name := valuativeRel) a:50 " ≤ᵥ " b:51 => binrel% ValuativeRel.rel a b
 
 namespace Valuation
 
@@ -120,7 +121,14 @@ lemma rel_mul_left {x y : R} (z) : x ≤ᵥ y → (z * x) ≤ᵥ (z * y) := by
 instance : Trans (rel (R := R)) (rel (R := R)) (rel (R := R)) where
   trans h1 h2 := rel_trans h1 h2
 
-lemma rel_mul {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : x * x' ≤ᵥ y * y' := by
+protected alias rel.trans := rel_trans
+
+lemma rel_trans' {x y z : R} (h1 : y ≤ᵥ z) (h2 : x ≤ᵥ y) : x ≤ᵥ z :=
+  h2.trans h1
+
+protected alias rel.trans' := rel_trans'
+
+lemma rel_mul {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : (x * x') ≤ᵥ y * y' := by
   calc x * x' ≤ᵥ x * y' := rel_mul_left _ h2
     _ ≤ᵥ y * y' := rel_mul_right _ h1
 
@@ -259,6 +267,10 @@ theorem ValueGroupWithZero.mk_one_one : ValueGroupWithZero.mk (1 : R) 1 = 1 :=
   ValueGroupWithZero.sound (by simp) (by simp)
 
 @[simp]
+theorem ValueGroupWithZero.mk_eq_one (x : R) (y : posSubmonoid R) :
+    ValueGroupWithZero.mk x y = 1 ↔ x ≤ᵥ y ∧ y ≤ᵥ x := by
+  simp [← mk_one_one, mk_eq_mk]
+
 theorem ValueGroupWithZero.lift_zero {α : Sort*} (f : R → posSubmonoid R → α)
     (hf : ∀ (x y : R) (t s : posSubmonoid R), x * t ≤ᵥ y * s → y * s ≤ᵥ x * t → f x s = f y t) :
     ValueGroupWithZero.lift f hf 0 = f 0 1 :=
@@ -592,6 +604,34 @@ variable (R) in
 class IsNontrivial where
   condition : ∃ γ : ValueGroupWithZero R, γ ≠ 0 ∧ γ ≠ 1
 
+lemma isNontrivial_iff_nontrivial_units :
+    IsNontrivial R ↔ Nontrivial (ValueGroupWithZero R)ˣ := by
+  constructor
+  · rintro ⟨γ, hγ, hγ'⟩
+    refine ⟨Units.mk0 _ hγ, 1, ?_⟩
+    simp [← Units.val_eq_one, hγ']
+  · rintro ⟨r, s, h⟩
+    rcases eq_or_ne r 1 with rfl | hr
+    · exact ⟨s.val, by simp, by simpa using h.symm⟩
+    · exact ⟨r.val, by simp, by simpa using hr⟩
+
+lemma isNontrivial_iff_isNontrivial :
+    IsNontrivial R ↔ (valuation R).IsNontrivial := by
+  constructor
+  · rintro ⟨r, hr, hr'⟩
+    induction r using ValueGroupWithZero.ind with | mk r s
+    by_cases hs : valuation R s = 1
+    · refine ⟨r, ?_, ?_⟩
+      · simpa [valuation] using hr
+      · simp only [ne_eq, ValueGroupWithZero.mk_eq_one, not_and, valuation, Valuation.coe_mk,
+          MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, OneMemClass.coe_one] at hr' hs ⊢
+        contrapose! hr'
+        exact hr'.imp hs.right.trans' hs.left.trans
+    · refine ⟨s, ?_, hs⟩
+      simp [valuation, ← posSubmonoid_def]
+  · rintro ⟨r, hr, hr'⟩
+    exact ⟨valuation R r, hr, hr'⟩
+
 variable (R) in
 /-- A ring with a valuative relation is discrete if its value group-with-zero
 has a maximal element `< 1`. -/

Mathlib/Topology/Algebra/Valued/NormedValued.lean

@@ -63,7 +63,7 @@ instance {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] :
     Valuation.RankOne (valuation (K := K)) where
   hom := .id _
   strictMono' := strictMono_id
-  nontrivial' := (exists_one_lt_norm K).imp fun x h ↦ by
+  exists_val_nontrivial := (exists_one_lt_norm K).imp fun x h ↦ by
     have h' : x ≠ 0 := norm_eq_zero.not.mp (h.gt.trans' (by simp)).ne'
     simp [valuation_apply, ← NNReal.coe_inj, h.ne', h']