feat: WithAbs type synonym (#17998)

This PR contains the type synonym `WithAbs`. This is a type synonym for a semiring `R` that depends on an absolute value `v : AbsoluteValue R S`, where `S` is an `OrderedSemiring`. This is used in order to handle ambiguities arising from multiple sources of instances. For example, each infinite place on a number field defines distinct uniform structures via their associated real absolute values. The `WithAbs` type synonym allows the type class inferencing system to automatically infer such dependent instances, making it simpler to define the Archimedean completions of a number field. See #16483 for this application along with prior feedback.

Author: Salvatore Mercuri

Mathlib.lean

@@ -817,6 +817,7 @@ import Mathlib.Algebra.Ring.Subsemiring.Pointwise
 import Mathlib.Algebra.Ring.SumsOfSquares
 import Mathlib.Algebra.Ring.ULift
 import Mathlib.Algebra.Ring.Units
+import Mathlib.Algebra.Ring.WithAbs
 import Mathlib.Algebra.Ring.WithZero
 import Mathlib.Algebra.RingQuot
 import Mathlib.Algebra.SMulWithZero

Mathlib/Algebra/Ring/WithAbs.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2024 Salvatore Mercuri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Salvatore Mercuri
+-/
+import Mathlib.Algebra.Group.Basic
+import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Analysis.Normed.Field.Basic
+
+/-!
+# WithAbs
+
+`WithAbs v` is a type synonym for a semiring `R` which depends on an absolute value. The point of
+this is to allow the type class inference system to handle multiple sources of instances that
+arise from absolute values. See `NumberTheory.NumberField.Completion` for an example of this
+being used to define Archimedean completions of a number field.
+
+## Main definitions
+ - `WithAbs` : type synonym for a semiring which depends on an absolute value. This is
+  a function that takes an absolute value on a semiring and returns the semiring. This can be used
+  to assign and infer instances on a semiring that depend on absolute values.
+ - `WithAbs.equiv v` : the canonical (type) equivalence between `WithAbs v` and `R`.
+ - `WithAbs.ringEquiv v` : The canonical ring equivalence between `WithAbs v` and `R`.
+-/
+noncomputable section
+
+variable {R S K : Type*} [Semiring R] [OrderedSemiring S] [Field K]
+
+/-- Type synonym for a semiring which depends on an absolute value. This is a function that takes
+an absolute value on a semiring and returns the semiring. We use this to assign and infer instances
+on a semiring that depend on absolute values. -/
+@[nolint unusedArguments]
+def WithAbs : AbsoluteValue R S → Type _ := fun _ => R
+
+namespace WithAbs
+
+variable (v : AbsoluteValue R ℝ)
+
+/-- Canonical equivalence between `WithAbs v` and `R`. -/
+def equiv : WithAbs v ≃ R := Equiv.refl (WithAbs v)
+
+instance instNonTrivial [Nontrivial R] : Nontrivial (WithAbs v) := inferInstanceAs (Nontrivial R)
+
+instance instUnique [Unique R] : Unique (WithAbs v) := inferInstanceAs (Unique R)
+
+instance instSemiring : Semiring (WithAbs v) := inferInstanceAs (Semiring R)
+
+instance instRing [Ring R] : Ring (WithAbs v) := inferInstanceAs (Ring R)
+
+instance instInhabited : Inhabited (WithAbs v) := ⟨0⟩
+
+instance normedRing {R : Type*} [Ring R] (v : AbsoluteValue R ℝ) : NormedRing (WithAbs v) :=
+  v.toNormedRing
+
+instance normedField (v : AbsoluteValue K ℝ) : NormedField (WithAbs v) :=
+  v.toNormedField
+
+/-! `WithAbs.equiv` preserves the ring structure. -/
+
+variable (x y : WithAbs v) (r s : R)
+@[simp]
+theorem equiv_zero : WithAbs.equiv v 0 = 0 := rfl
+
+@[simp]
+theorem equiv_symm_zero : (WithAbs.equiv v).symm 0 = 0 := rfl
+
+@[simp]
+theorem equiv_add : WithAbs.equiv v (x + y) = WithAbs.equiv v x + WithAbs.equiv v y := rfl
+
+@[simp]
+theorem equiv_symm_add :
+    (WithAbs.equiv v).symm (r + s) = (WithAbs.equiv v).symm r + (WithAbs.equiv v).symm s :=
+  rfl
+
+@[simp]
+theorem equiv_sub [Ring R] : WithAbs.equiv v (x - y) = WithAbs.equiv v x - WithAbs.equiv v y := rfl
+
+@[simp]
+theorem equiv_symm_sub [Ring R] :
+    (WithAbs.equiv v).symm (r - s) = (WithAbs.equiv v).symm r - (WithAbs.equiv v).symm s :=
+  rfl
+
+@[simp]
+theorem equiv_neg [Ring R] : WithAbs.equiv v (-x) = - WithAbs.equiv v x := rfl
+
+@[simp]
+theorem equiv_symm_neg [Ring R] : (WithAbs.equiv v).symm (-r) = - (WithAbs.equiv v).symm r := rfl
+
+@[simp]
+theorem equiv_mul : WithAbs.equiv v (x * y) = WithAbs.equiv v x * WithAbs.equiv v y := rfl
+
+@[simp]
+theorem equiv_symm_mul :
+    (WithAbs.equiv v).symm (x * y) = (WithAbs.equiv v).symm x * (WithAbs.equiv v).symm y :=
+  rfl
+
+/-- `WithAbs.equiv` as a ring equivalence. -/
+def ringEquiv : WithAbs v ≃+* R := RingEquiv.refl _
+
+end WithAbs

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -17,6 +17,11 @@ definitions.
 
 Some useful results that relate the topology of the normed field to the discrete topology include:
 * `norm_eq_one_iff_ne_zero_of_discrete`
+
+Methods for constructing a normed ring/field instance from a given real absolute value on a
+ring/field are given in:
+* AbsoluteValue.toNormedRing
+* AbsoluteValue.toNormedField
 -/
 
 -- Guard against import creep.
@@ -1090,3 +1095,25 @@ instance toNormedCommRing [NormedCommRing R] [SubringClass S R] (s : S) : Normed
   { SubringClass.toNormedRing s with mul_comm := mul_comm }
 
 end SubringClass
+
+namespace AbsoluteValue
+
+/-- A real absolute value on a ring determines a `NormedRing` structure. -/
+noncomputable def toNormedRing {R : Type*} [Ring R] (v : AbsoluteValue R ℝ) : NormedRing R where
+  norm := v
+  dist_eq _ _ := rfl
+  dist_self x := by simp only [sub_self, MulHom.toFun_eq_coe, AbsoluteValue.coe_toMulHom, map_zero]
+  dist_comm := v.map_sub
+  dist_triangle := v.sub_le
+  edist_dist x y := rfl
+  norm_mul x y := (v.map_mul x y).le
+  eq_of_dist_eq_zero := by simp only [MulHom.toFun_eq_coe, AbsoluteValue.coe_toMulHom,
+    AbsoluteValue.map_sub_eq_zero_iff, imp_self, implies_true]
+
+/-- A real absolute value on a field determines a `NormedField` structure. -/
+noncomputable def toNormedField {K : Type*} [Field K] (v : AbsoluteValue K ℝ) : NormedField K where
+  toField := inferInstanceAs (Field K)
+  __ := v.toNormedRing
+  norm_mul' := v.map_mul
+
+end AbsoluteValue