feat(algebra/*, ring_theory/valuation/basic): `linear_ordered_add_com…

…m_group_with_top`, `add_valuation.map_sub` (#7452)

Defines `linear_ordered_add_comm_group_with_top`
Uses that to port a few more facts about `valuation`s to `add_valuation`s.

src/algebra/linear_ordered_comm_group_with_zero.lean

@@ -44,6 +44,14 @@ instance [linear_ordered_add_comm_monoid_with_top α] :
   ..multiplicative.ordered_comm_monoid,
   ..multiplicative.linear_order }
 
+instance [linear_ordered_add_comm_group_with_top α] :
+  linear_ordered_comm_group_with_zero (multiplicative (order_dual α)) :=
+{ inv_zero := linear_ordered_add_comm_group_with_top.neg_top,
+  mul_inv_cancel := linear_ordered_add_comm_group_with_top.add_neg_cancel,
+  ..multiplicative.div_inv_monoid,
+  ..multiplicative.linear_ordered_comm_monoid_with_zero,
+  ..multiplicative.nontrivial }
+
 section linear_ordered_comm_monoid
 
 variables [linear_ordered_comm_monoid_with_zero α]
@@ -196,6 +204,13 @@ lemma inv_lt_inv'' (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ < b⁻¹ ↔ b < a :=
 lemma inv_le_inv'' (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
 @inv_le_inv_iff _ _ (units.mk0 a ha) (units.mk0 b hb)
 
+instance : linear_ordered_add_comm_group_with_top (additive (order_dual α)) :=
+{ neg_top := inv_zero,
+  add_neg_cancel := λ a ha, mul_inv_cancel ha,
+  ..additive.sub_neg_monoid,
+  ..additive.linear_ordered_add_comm_monoid_with_top,
+  ..additive.nontrivial }
+
 namespace monoid_hom
 
 variables {R : Type*} [ring R] (f : R →* α)

src/algebra/ordered_group.lean

@@ -567,6 +567,14 @@ addition is monotone. -/
 class linear_ordered_add_comm_group (α : Type u) extends add_comm_group α, linear_order α :=
 (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
 
+/-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
+  Instances should include number systems with an infinite element adjoined.` -/
+@[protect_proj, ancestor linear_ordered_add_comm_monoid_with_top sub_neg_monoid nontrivial]
+class linear_ordered_add_comm_group_with_top (α : Type*)
+  extends linear_ordered_add_comm_monoid_with_top α, sub_neg_monoid α, nontrivial α :=
+(neg_top : - (⊤ : α) = ⊤)
+(add_neg_cancel : ∀ a:α, a ≠ ⊤ → a + (- a) = 0)
+
 /-- A linearly ordered commutative group is a
 commutative group with a linear order in which
 multiplication is monotone. -/
@@ -861,6 +869,18 @@ abs_sub_le_iff.2 ⟨sub_le_sub hau hbl, sub_le_sub hbu hal⟩
 lemma eq_of_abs_sub_nonpos (h : abs (a - b) ≤ 0) : a = b :=
 eq_of_abs_sub_eq_zero (le_antisymm h (abs_nonneg (a - b)))
 
+instance with_top.linear_ordered_add_comm_group_with_top :
+  linear_ordered_add_comm_group_with_top (with_top α) :=
+{ neg := option.map (λ a : α, -a),
+  neg_top := @option.map_none _ _ (λ a : α, -a),
+  add_neg_cancel := begin
+    rintro (a | a) ha,
+    { exact (ha rfl).elim },
+    exact with_top.coe_add.symm.trans (with_top.coe_eq_coe.2 (add_neg_self a)),
+  end,
+  .. with_top.linear_ordered_add_comm_monoid_with_top,
+  .. option.nontrivial }
+
 end linear_ordered_add_comm_group
 
 /-- This is not so much a new structure as a construction mechanism

src/algebra/ordered_monoid.lean

@@ -1288,4 +1288,10 @@ instance [linear_ordered_comm_monoid α] : linear_ordered_add_comm_monoid (addit
 { ..additive.linear_order,
   ..additive.ordered_add_comm_monoid }
 
+instance [sub_neg_monoid α] : sub_neg_monoid (order_dual α) :=
+{ ..show sub_neg_monoid α, by apply_instance }
+
+instance [div_inv_monoid α] : div_inv_monoid (order_dual α) :=
+{ ..show div_inv_monoid α, by apply_instance }
+
 end type_tags

src/ring_theory/valuation/basic.lean

@@ -202,11 +202,17 @@ v.to_monoid_with_zero_hom.to_monoid_hom.map_neg x
 lemma map_sub_swap (x y : R) : v (x - y) = v (y - x) :=
 v.to_monoid_with_zero_hom.to_monoid_hom.map_sub_swap x y
 
-lemma map_sub_le_max (x y : R) : v (x - y) ≤ max (v x) (v y) :=
+lemma map_sub (x y : R) : v (x - y) ≤ max (v x) (v y) :=
 calc v (x - y) = v (x + -y)         : by rw [sub_eq_add_neg]
            ... ≤ max (v x) (v $ -y) : v.map_add _ _
            ... = max (v x) (v y)    : by rw map_neg
 
+lemma map_sub_le {x y g} (hx : v x ≤ g) (hy : v y ≤ g) : v (x - y) ≤ g :=
+begin
+  rw sub_eq_add_neg,
+  exact v.map_add_le hx (le_trans (le_of_eq (v.map_neg y)) hy)
+end
+
 lemma map_add_of_distinct_val (h : v x ≠ v y) : v (x + y) = max (v x) (v y) :=
 begin
   suffices : ¬v (x + y) < max (v x) (v y),
@@ -217,7 +223,7 @@ begin
   { rw max_eq_left_of_lt vyx at h',
     apply lt_irrefl (v x),
     calc v x = v ((x+y) - y)         : by simp
-         ... ≤ max (v $ x + y) (v y) : map_sub_le_max _ _ _
+         ... ≤ max (v $ x + y) (v y) : map_sub _ _ _
          ... < v x                   : max_lt h' vyx },
   { apply this h.symm,
     rwa [add_comm, max_comm] at h' }
@@ -425,11 +431,13 @@ def add_valuation := valuation R (multiplicative (order_dual Γ₀))
 end add_monoid
 
 namespace add_valuation
-variables {Γ₀   : Type*} [linear_ordered_add_comm_monoid_with_top Γ₀]
-variables {Γ'₀  : Type*} [linear_ordered_add_comm_monoid_with_top Γ'₀]
+variables {Γ₀   : Type*} {Γ'₀  : Type*}
 
 section basic
 
+section monoid
+
+variables [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀]
 variables (R) (Γ₀) [ring R]
 
 /-- A valuation is coerced to the underlying function `R → Γ₀`. -/
@@ -525,9 +533,41 @@ v.map {
 def is_equiv (v₁ : add_valuation R Γ₀) (v₂ : add_valuation R Γ'₀) : Prop :=
 v₁.is_equiv v₂
 
+end monoid
+
+section group
+variables [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {x y z : R}
+
+@[simp] lemma map_inv {K : Type*} [division_ring K]
+  (v : add_valuation K Γ₀) {x : K} : v x⁻¹ = - (v x) :=
+v.map_inv
+
+lemma map_units_inv (x : units R) : v (x⁻¹ : units R) = - (v x) :=
+v.map_units_inv x
+
+@[simp] lemma map_neg (x : R) : v (-x) = v x :=
+v.map_neg x
+
+lemma map_sub_swap (x y : R) : v (x - y) = v (y - x) :=
+v.map_sub_swap x y
+
+lemma map_sub (x y : R) : min (v x) (v y) ≤ v (x - y) :=
+v.map_sub x y
+
+lemma map_le_sub {x y g} (hx : g ≤ v x) (hy : g ≤ v y) : g ≤ v (x - y) := v.map_sub_le hx hy
+
+lemma map_add_of_distinct_val (h : v x ≠ v y) : v (x + y) = min (v x) (v y) :=
+v.map_add_of_distinct_val h
+
+lemma map_eq_of_lt_sub (h : v x < v (y - x)) : v y = v x :=
+v.map_eq_of_sub_lt h
+
+end group
+
 end basic
 
 namespace is_equiv
+variables [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀]
 variables [ring R]
 variables {Γ''₀ : Type*} [linear_ordered_add_comm_monoid_with_top Γ''₀]
 variables {v : add_valuation R Γ₀}
@@ -568,6 +608,7 @@ h.ne_zero
 end is_equiv
 
 section supp
+variables [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀]
 variables [comm_ring R]
 variables (v : add_valuation R Γ₀)
 
@@ -614,4 +655,6 @@ v.supp_quot_supp
 
 end supp -- end of section
 
+attribute [irreducible] add_valuation
+
 end add_valuation