feat(RingTheory/Valuation/RankOne): add rank one valuations (#12156)

Add the definition of rank one valuation, as well as some basic lemmas.



Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Author: mariainesdff

Mathlib.lean

@@ -3523,6 +3523,7 @@ import Mathlib.RingTheory.Valuation.Integral
 import Mathlib.RingTheory.Valuation.PrimeMultiplicity
 import Mathlib.RingTheory.Valuation.Quotient
 import Mathlib.RingTheory.Valuation.RamificationGroup
+import Mathlib.RingTheory.Valuation.RankOne
 import Mathlib.RingTheory.Valuation.ValuationRing
 import Mathlib.RingTheory.Valuation.ValuationSubring
 import Mathlib.RingTheory.WittVector.Basic

Mathlib/RingTheory/Valuation/RankOne.lean

@@ -0,0 +1,73 @@
+/-
+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.Real.NNReal
+import Mathlib.RingTheory.Valuation.Basic
+
+/-!
+# Rank one valuations
+
+We define rank one valuations.
+
+## Main Definitions
+* `RankOne` : A valuation `v` has rank one if it is nontrivial and its image is contained in `ℝ≥0`.
+  Note that this class contains the data of the inclusion of the codomain of `v` into `ℝ≥0`.
+
+## Tags
+
+valuation, rank one
+-/
+
+noncomputable section
+
+open Function Multiplicative
+
+open scoped NNReal
+
+variable {R : Type*} [Ring R] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+
+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
+  /-- 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'
+
+/-- If `v` is a rank one valuation and `x : Γ₀` has image `0` under `RankOne.hom v`, then
+  `x = 0`. -/
+theorem zero_of_hom_zero {x : Γ₀} (hx : hom v x = 0) : x = 0 := by
+  refine (eq_of_le_of_not_lt (zero_le' (a := x)) fun h_lt ↦ ?_).symm
+  have hs := strictMono v h_lt
+  rw [_root_.map_zero, hx] at hs
+  exact hs.false
+
+/-- If `v` is a rank one valuation, then`x : Γ₀` has image `0` under `RankOne.hom v` if and
+  only if `x = 0`. -/
+theorem hom_eq_zero_iff {x : Γ₀} : RankOne.hom v x = 0 ↔ x = 0 :=
+  ⟨fun h ↦ zero_of_hom_zero v h, fun h ↦ by rw [h, _root_.map_zero]⟩
+
+/-- A nontrivial unit of `Γ₀`, given that there exists a rank one `v : Valuation R Γ₀`. -/
+def unit : Γ₀ˣ :=
+  Units.mk0 (v (nontrivial v).choose) ((nontrivial v).choose_spec).1
+
+/-- A proof that `RankOne.unit v ≠ 1`. -/
+theorem unit_ne_one : unit v ≠ 1 := by
+  rw [Ne.def, ← Units.eq_iff, Units.val_one]
+  exact ((nontrivial v).choose_spec ).2
+
+end RankOne
+
+end Valuation