split(algebra/order/nonneg): Separate ring and field instances (#…

…17348)

Split `algebra.order.nonneg` into:
* `algebra.order.nonneg.ring` for ring instances
* `algebra.order.nonneg.field` for field and archimedean instances

src/algebra/order/nonneg/field.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2021 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import algebra.order.archimedean
+import algebra.order.nonneg.ring
+
+/-!
+# Semifield structure on the type of nonnegative elements
+
+This file defines instances and prove some properties about the nonnegative elements
+`{x : α // 0 ≤ x}` of an arbitrary type `α`.
+
+This is used to derive algebraic structures on `ℝ≥0` and `ℚ≥0` automatically.
+
+## Main declarations
+
+* `{x : α // 0 ≤ x}` is a `canonically_linear_ordered_semifield` if `α` is a `linear_ordered_field`.
+-/
+
+open set
+
+variables {α : Type*}
+
+namespace nonneg
+
+section linear_ordered_semifield
+variables [linear_ordered_semifield α] {x y : α}
+
+instance has_inv : has_inv {x : α // 0 ≤ x} := ⟨λ x, ⟨x⁻¹, inv_nonneg.2 x.2⟩⟩
+
+@[simp, norm_cast]
+protected lemma coe_inv (a : {x : α // 0 ≤ x}) : ((a⁻¹ : {x : α // 0 ≤ x}) : α) = a⁻¹ := rfl
+
+@[simp] lemma inv_mk (hx : 0 ≤ x) : (⟨x, hx⟩ : {x : α // 0 ≤ x})⁻¹ = ⟨x⁻¹, inv_nonneg.2 hx⟩ := rfl
+
+instance has_div : has_div {x : α // 0 ≤ x} := ⟨λ x y, ⟨x / y, div_nonneg x.2 y.2⟩⟩
+
+@[simp, norm_cast] protected lemma coe_div (a b : {x : α // 0 ≤ x}) :
+  ((a / b : {x : α // 0 ≤ x}) : α) = a / b := rfl
+
+@[simp] lemma mk_div_mk (hx : 0 ≤ x) (hy : 0 ≤ y) :
+  (⟨x, hx⟩ : {x : α // 0 ≤ x}) / ⟨y, hy⟩ = ⟨x / y, div_nonneg hx hy⟩ := rfl
+
+instance has_zpow : has_pow {x : α // 0 ≤ x} ℤ := ⟨λ a n, ⟨a ^ n, zpow_nonneg a.2 _⟩⟩
+
+@[simp, norm_cast] protected lemma coe_zpow (a : {x : α // 0 ≤ x}) (n : ℤ) :
+  ((a ^ n : {x : α // 0 ≤ x}) : α) = a ^ n := rfl
+
+@[simp] lemma mk_zpow (hx : 0 ≤ x) (n : ℤ) :
+  (⟨x, hx⟩ : {x : α // 0 ≤ x}) ^ n = ⟨x ^ n, zpow_nonneg hx n⟩ := rfl
+
+instance linear_ordered_semifield : linear_ordered_semifield {x : α // 0 ≤ x} :=
+subtype.coe_injective.linear_ordered_semifield _ nonneg.coe_zero nonneg.coe_one nonneg.coe_add
+    nonneg.coe_mul nonneg.coe_inv nonneg.coe_div (λ _ _, rfl) nonneg.coe_pow nonneg.coe_zpow
+    nonneg.coe_nat_cast (λ _ _, rfl) (λ _ _, rfl)
+
+end linear_ordered_semifield
+
+instance canonically_linear_ordered_semifield [linear_ordered_field α] :
+  canonically_linear_ordered_semifield {x : α // 0 ≤ x} :=
+{ ..nonneg.linear_ordered_semifield, ..nonneg.canonically_ordered_comm_semiring }
+
+instance linear_ordered_comm_group_with_zero [linear_ordered_field α] :
+  linear_ordered_comm_group_with_zero {x : α // 0 ≤ x} :=
+infer_instance
+
+/-! ### Floor -/
+
+instance archimedean [ordered_add_comm_monoid α] [archimedean α] : archimedean {x : α // 0 ≤ x} :=
+⟨λ x y hy,
+  let ⟨n, hr⟩ := archimedean.arch (x : α) (hy : (0 : α) < y) in
+  ⟨n, show (x : α) ≤ (n • y : {x : α // 0 ≤ x}), by simp [*, -nsmul_eq_mul, nsmul_coe]⟩⟩
+
+instance floor_semiring [ordered_semiring α] [floor_semiring α] : floor_semiring {r : α // 0 ≤ r} :=
+{ floor := λ a, ⌊(a : α)⌋₊,
+  ceil := λ a, ⌈(a : α)⌉₊,
+  floor_of_neg := λ a ha, floor_semiring.floor_of_neg ha,
+  gc_floor := λ a n ha, begin
+    refine (floor_semiring.gc_floor (show 0 ≤ (a : α), from ha)).trans _,
+    rw [←subtype.coe_le_coe, nonneg.coe_nat_cast]
+  end,
+  gc_ceil := λ a n, begin
+    refine (floor_semiring.gc_ceil (a : α) n).trans _,
+    rw [←subtype.coe_le_coe, nonneg.coe_nat_cast]
+  end}
+
+@[norm_cast] lemma nat_floor_coe [ordered_semiring α] [floor_semiring α] (a : {r : α // 0 ≤ r}) :
+  ⌊(a : α)⌋₊ = ⌊a⌋₊ := rfl
+
+@[norm_cast] lemma nat_ceil_coe [ordered_semiring α] [floor_semiring α] (a : {r : α // 0 ≤ r}) :
+  ⌈(a : α)⌉₊ = ⌈a⌉₊  := rfl
+
+end nonneg

src/algebra/order/nonneg.lean → src/algebra/order/nonneg/ring.lean

@@ -3,9 +3,9 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import algebra.order.archimedean
-import order.lattice_intervals
+import algebra.order.ring
 import order.complete_lattice_intervals
+import order.lattice_intervals
 
 /-!
 # The type of nonnegative elements
@@ -20,7 +20,6 @@ When `α` is `ℝ`, this will give us some properties about `ℝ≥0`.
 ## Main declarations
 
 * `{x : α // 0 ≤ x}` is a `canonically_linear_ordered_add_monoid` if `α` is a `linear_ordered_ring`.
-* `{x : α // 0 ≤ x}` is a `linear_ordered_comm_group_with_zero` if `α` is a `linear_ordered_field`.
 
 ## Implementation Notes
 
@@ -149,11 +148,6 @@ lemma nsmul_coe [ordered_add_comm_monoid α] (n : ℕ) (r : {x : α // 0 ≤ x})
   ↑(n • r) = n • (r : α) :=
 nonneg.coe_add_monoid_hom.map_nsmul _ _
 
-instance archimedean [ordered_add_comm_monoid α] [archimedean α] : archimedean {x : α // 0 ≤ x} :=
-⟨ assume x y pos_y,
-  let ⟨n, hr⟩ := archimedean.arch (x : α) (pos_y : (0 : α) < y) in
-  ⟨n, show (x : α) ≤ (n • y : {x : α // 0 ≤ x}), by simp [*, -nsmul_eq_mul, nsmul_coe]⟩ ⟩
-
 instance has_one [ordered_semiring α] : has_one {x : α // 0 ≤ x} :=
 { one := ⟨1, zero_le_one⟩ }
 
@@ -181,16 +175,21 @@ instance add_monoid_with_one [ordered_semiring α] : add_monoid_with_one {x : α
   nat_cast_succ := λ _, by simp [nat.cast]; refl,
   .. nonneg.has_one, .. nonneg.ordered_add_comm_monoid }
 
+@[simp, norm_cast]
+protected lemma coe_nat_cast [ordered_semiring α] (n : ℕ) : ((↑n : {x : α // 0 ≤ x}) : α) = n := rfl
+
+@[simp] lemma mk_nat_cast [ordered_semiring α] (n : ℕ) :
+  (⟨n, n.cast_nonneg⟩ : {x : α // 0 ≤ x}) = n := rfl
+
 instance has_pow [ordered_semiring α] : has_pow {x : α // 0 ≤ x} ℕ :=
 { pow := λ x n, ⟨x ^ n, pow_nonneg x.2 n⟩ }
 
 @[simp, norm_cast]
 protected lemma coe_pow [ordered_semiring α] (a : {x : α // 0 ≤ x}) (n : ℕ) :
-  ((a ^ n: {x : α // 0 ≤ x}) : α) = a ^ n := rfl
+  (↑(a ^ n) : α) = a ^ n := rfl
 
 @[simp] lemma mk_pow [ordered_semiring α] {x : α} (hx : 0 ≤ x) (n : ℕ) :
-  (⟨x, hx⟩ : {x : α // 0 ≤ x}) ^ n = ⟨x ^ n, pow_nonneg hx n⟩ :=
-rfl
+  (⟨x, hx⟩ : {x : α // 0 ≤ x}) ^ n = ⟨x ^ n, pow_nonneg hx n⟩ := rfl
 
 instance ordered_semiring [ordered_semiring α] : ordered_semiring {x : α // 0 ≤ x} :=
 subtype.coe_injective.ordered_semiring _
@@ -239,10 +238,6 @@ instance linear_ordered_comm_monoid_with_zero [linear_ordered_comm_ring α] :
 def coe_ring_hom [ordered_semiring α] : {x : α // 0 ≤ x} →+* α :=
 ⟨coe, nonneg.coe_one, nonneg.coe_mul, nonneg.coe_zero, nonneg.coe_add⟩
 
-@[simp, norm_cast]
-protected lemma coe_nat_cast [ordered_semiring α] (n : ℕ) : ((↑n : {x : α // 0 ≤ x}) : α) = n :=
-map_nat_cast (coe_ring_hom : {x : α // 0 ≤ x} →+* α) n
-
 instance canonically_ordered_add_monoid [ordered_ring α] :
   canonically_ordered_add_monoid {x : α // 0 ≤ x} :=
 { le_self_add := λ a b, le_add_of_nonneg_right b.2,
@@ -261,70 +256,6 @@ instance canonically_linear_ordered_add_monoid [linear_ordered_ring α] :
   canonically_linear_ordered_add_monoid {x : α // 0 ≤ x} :=
 { ..subtype.linear_order _, ..nonneg.canonically_ordered_add_monoid }
 
-section linear_ordered_semifield
-variables [linear_ordered_semifield α] {x y : α}
-
-instance has_inv : has_inv {x : α // 0 ≤ x} := ⟨λ x, ⟨x⁻¹, inv_nonneg.mpr x.2⟩⟩
-
-@[simp, norm_cast]
-protected lemma coe_inv (a : {x : α // 0 ≤ x}) : ((a⁻¹ : {x : α // 0 ≤ x}) : α) = a⁻¹ := rfl
-
-@[simp] lemma inv_mk (hx : 0 ≤ x) : (⟨x, hx⟩ : {x : α // 0 ≤ x})⁻¹ = ⟨x⁻¹, inv_nonneg.mpr hx⟩ := rfl
-
-instance has_div : has_div {x : α // 0 ≤ x} := ⟨λ x y, ⟨x / y, div_nonneg x.2 y.2⟩⟩
-
-@[simp, norm_cast] protected lemma coe_div (a b : {x : α // 0 ≤ x}) :
-  ((a / b : {x : α // 0 ≤ x}) : α) = a / b := rfl
-
-@[simp] lemma mk_div_mk (hx : 0 ≤ x) (hy : 0 ≤ y) :
-  (⟨x, hx⟩ : {x : α // 0 ≤ x}) / ⟨y, hy⟩ = ⟨x / y, div_nonneg hx hy⟩ := rfl
-
-instance has_zpow : has_pow {x : α // 0 ≤ x} ℤ := ⟨λ a n, ⟨a ^ n, zpow_nonneg a.2 _⟩⟩
-
-@[simp, norm_cast] protected lemma coe_zpow (a : {x : α // 0 ≤ x}) (n : ℤ) :
-  ((a ^ n : {x : α // 0 ≤ x}) : α) = a ^ n := rfl
-
-@[simp] lemma mk_zpow (hx : 0 ≤ x) (n : ℤ) :
-  (⟨x, hx⟩ : {x : α // 0 ≤ x}) ^ n = ⟨x ^ n, zpow_nonneg hx n⟩ := rfl
-
-instance linear_ordered_semifield : linear_ordered_semifield {x : α // 0 ≤ x} :=
-subtype.coe_injective.linear_ordered_semifield _ nonneg.coe_zero nonneg.coe_one nonneg.coe_add
-    nonneg.coe_mul nonneg.coe_inv nonneg.coe_div (λ _ _, rfl) nonneg.coe_pow nonneg.coe_zpow
-    nonneg.coe_nat_cast (λ _ _, rfl) (λ _ _, rfl)
-
-end linear_ordered_semifield
-
-instance linear_ordered_comm_group_with_zero [linear_ordered_field α] :
-  linear_ordered_comm_group_with_zero {x : α // 0 ≤ x} :=
-{ inv_zero := by { ext, exact inv_zero },
-  mul_inv_cancel := by { intros a ha, ext, refine mul_inv_cancel (mt (λ h, _) ha), ext, exact h },
-  ..nonneg.nontrivial,
-  ..nonneg.has_inv,
-  ..nonneg.linear_ordered_comm_monoid_with_zero }
-
-instance canonically_linear_ordered_semifield [linear_ordered_field α] :
-  canonically_linear_ordered_semifield {x : α // 0 ≤ x} :=
-{ ..nonneg.linear_ordered_semifield, ..nonneg.canonically_ordered_comm_semiring }
-
-instance floor_semiring [ordered_semiring α] [floor_semiring α] : floor_semiring {r : α // 0 ≤ r} :=
-{ floor := λ a, ⌊(a : α)⌋₊,
-  ceil := λ a, ⌈(a : α)⌉₊,
-  floor_of_neg := λ a ha, floor_semiring.floor_of_neg ha,
-  gc_floor := λ a n ha, begin
-    refine (floor_semiring.gc_floor (show 0 ≤ (a : α), from ha)).trans _,
-    rw [←subtype.coe_le_coe, nonneg.coe_nat_cast]
-  end,
-  gc_ceil := λ a n, begin
-    refine (floor_semiring.gc_ceil (a : α) n).trans _,
-    rw [←subtype.coe_le_coe, nonneg.coe_nat_cast]
-  end}
-
-@[norm_cast] lemma nat_floor_coe [ordered_semiring α] [floor_semiring α] (a : {r : α // 0 ≤ r}) :
-  ⌊(a : α)⌋₊ = ⌊a⌋₊ := rfl
-
-@[norm_cast] lemma nat_ceil_coe [ordered_semiring α] [floor_semiring α] (a : {r : α // 0 ≤ r}) :
-  ⌈(a : α)⌉₊ = ⌈a⌉₊  := rfl
-
 section linear_order
 
 variables [has_zero α] [linear_order α]

src/data/rat/nnrat.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import algebra.algebra.basic
-import algebra.order.nonneg
+import algebra.order.nonneg.field
 
 /-!
 # Nonnegative rationals

src/data/real/nnreal.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import algebra.algebra.basic
-import algebra.order.nonneg
+import algebra.order.nonneg.field
 import data.real.pointwise
 import tactic.positivity