feat(algebra/order/positive): new file (#14833)

Define various algebraic structures on the set of positive numbers.

I have two reasons to introduce these classes:

- we can use `{x : ℝ // 0 < x}` in various filter bases; this may save us from explicit usage of `half_pos` or `div_pos` here or there;
- I want to introduce a multiplicative action of `{x : ℝ // 0 < x}` on the upper half plane.

Author: urkud

src/algebra/order/positive/field.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import algebra.order.positive.ring
+import algebra.field_power
+
+/-!
+# Algebraic structures on the set of positive numbers
+
+In this file we prove that the set of positive elements of a linear ordered field is a linear
+ordered commutative group.
+-/
+
+variables {K : Type*} [linear_ordered_field K]
+
+namespace positive
+
+instance : has_inv {x : K // 0 < x} := ⟨λ x, ⟨x⁻¹, inv_pos.2 x.2⟩⟩
+
+@[simp] lemma coe_inv (x : {x : K // 0 < x}) : ↑x⁻¹ = (x⁻¹ : K) := rfl
+
+instance : has_pow {x : K // 0 < x} ℤ :=
+⟨λ x n, ⟨x ^ n, zpow_pos_of_pos x.2 _⟩⟩
+
+@[simp] lemma coe_zpow (x : {x : K // 0 < x}) (n : ℤ) : ↑(x ^ n) = (x ^ n : K) := rfl
+
+instance : linear_ordered_comm_group {x : K // 0 < x} :=
+{ mul_left_inv := λ a, subtype.ext $ inv_mul_cancel a.2.ne',
+  .. positive.subtype.has_inv, .. positive.subtype.linear_ordered_cancel_comm_monoid }
+
+end positive

src/algebra/order/positive/ring.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import algebra.order.ring
+
+/-!
+# Algebraic structures on the set of positive numbers
+
+In this file we define various instances (`add_semigroup`, `ordered_comm_monoid` etc) on the
+type `{x : R // 0 < x}`. In each case we try to require the weakest possible typeclass
+assumptions on `R` but possibly, there is a room for improvements.
+-/
+open function
+
+namespace positive
+
+variables {M R K : Type*}
+
+section add_basic
+
+variables [add_monoid M] [preorder M] [covariant_class M M (+) (<)]
+
+instance : has_add {x : M // 0 < x} := ⟨λ x y, ⟨x + y, add_pos x.2 y.2⟩⟩
+
+@[simp, norm_cast] lemma coe_add (x y : {x : M // 0 < x}) : ↑(x + y) = (x + y : M) := rfl
+
+instance : add_semigroup {x : M // 0 < x} := subtype.coe_injective.add_semigroup _ coe_add
+
+instance {M : Type*} [add_comm_monoid M] [preorder M] [covariant_class M M (+) (<)] :
+  add_comm_semigroup {x : M // 0 < x} :=
+subtype.coe_injective.add_comm_semigroup _ coe_add
+
+instance {M : Type*} [add_left_cancel_monoid M] [preorder M] [covariant_class M M (+) (<)] :
+  add_left_cancel_semigroup {x : M // 0 < x} :=
+subtype.coe_injective.add_left_cancel_semigroup _ coe_add
+
+instance {M : Type*} [add_right_cancel_monoid M] [preorder M] [covariant_class M M (+) (<)] :
+  add_right_cancel_semigroup {x : M // 0 < x} :=
+subtype.coe_injective.add_right_cancel_semigroup _ coe_add
+
+instance covariant_class_add_lt : covariant_class {x : M // 0 < x} {x : M // 0 < x} (+) (<) :=
+⟨λ x y z hyz, subtype.coe_lt_coe.1 $ add_lt_add_left hyz _⟩
+
+instance covariant_class_swap_add_lt [covariant_class M M (swap (+)) (<)] :
+  covariant_class {x : M // 0 < x} {x : M // 0 < x} (swap (+)) (<) :=
+⟨λ x y z hyz, subtype.coe_lt_coe.1 $ add_lt_add_right hyz _⟩
+
+instance contravariant_class_add_lt [contravariant_class M M (+) (<)] :
+  contravariant_class {x : M // 0 < x} {x : M // 0 < x} (+) (<) :=
+⟨λ x y z h, subtype.coe_lt_coe.1 $ lt_of_add_lt_add_left h⟩
+
+instance contravariant_class_swap_add_lt [contravariant_class M M (swap (+)) (<)] :
+  contravariant_class {x : M // 0 < x} {x : M // 0 < x} (swap (+)) (<) :=
+⟨λ x y z h, subtype.coe_lt_coe.1 $ lt_of_add_lt_add_right h⟩
+
+instance contravariant_class_add_le [contravariant_class M M (+) (≤)] :
+  contravariant_class {x : M // 0 < x} {x : M // 0 < x} (+) (≤) :=
+⟨λ x y z h, subtype.coe_le_coe.1 $ le_of_add_le_add_left h⟩
+
+instance contravariant_class_swap_add_le [contravariant_class M M (swap (+)) (≤)] :
+  contravariant_class {x : M // 0 < x} {x : M // 0 < x} (swap (+)) (≤) :=
+⟨λ x y z h, subtype.coe_le_coe.1 $ le_of_add_le_add_right h⟩
+
+end add_basic
+
+instance covariant_class_add_le [add_monoid M] [partial_order M] [covariant_class M M (+) (<)] :
+  covariant_class {x : M // 0 < x} {x : M // 0 < x} (+) (≤) :=
+⟨λ x, strict_mono.monotone $ λ _ _ h, add_lt_add_left h _⟩
+
+section mul
+
+variables [ordered_semiring R]
+
+instance : has_mul {x : R // 0 < x} := ⟨λ x y, ⟨x * y, mul_pos x.2 y.2⟩⟩
+
+@[simp] lemma coe_mul (x y : {x : R // 0 < x}) : ↑(x * y) = (x * y : R) := rfl
+
+instance : has_pow {x : R // 0 < x} ℕ := ⟨λ x n, ⟨x ^ n, pow_pos x.2 n⟩⟩
+
+@[simp] lemma coe_pow (x : {x : R // 0 < x}) (n : ℕ) : ↑(x ^ n) = (x ^ n : R) := rfl
+
+instance : semigroup {x : R // 0 < x} := subtype.coe_injective.semigroup coe coe_mul
+
+instance : distrib {x : R // 0 < x} := subtype.coe_injective.distrib _ coe_add coe_mul
+
+instance [nontrivial R] : has_one {x : R // 0 < x} := ⟨⟨1, one_pos⟩⟩
+
+@[simp] lemma coe_one [nontrivial R] : ((1 : {x : R // 0 < x}) : R) = 1 := rfl
+
+instance [nontrivial R] : monoid {x : R // 0 < x} :=
+subtype.coe_injective.monoid _ coe_one coe_mul coe_pow
+
+end mul
+
+section mul_comm
+
+instance [ordered_comm_semiring R] [nontrivial R] : ordered_comm_monoid {x : R // 0 < x} :=
+{ mul_le_mul_left := λ x y hxy c, subtype.coe_le_coe.1 $ mul_le_mul_of_nonneg_left hxy c.2.le,
+  .. subtype.partial_order _,
+  .. subtype.coe_injective.comm_monoid (coe : {x : R // 0 < x} → R) coe_one coe_mul coe_pow }
+
+/-- If `R` is a nontrivial linear ordered commutative semiring, then `{x : R // 0 < x}` is a linear
+ordered cancellative commutative monoid. We don't have a typeclass for linear ordered commutative
+semirings, so we assume `[linear_ordered_semiring R] [is_commutative R (*)] instead. -/
+instance [linear_ordered_semiring R] [is_commutative R (*)] [nontrivial R] :
+  linear_ordered_cancel_comm_monoid {x : R // 0 < x} :=
+{ mul_left_cancel := λ a b c h, subtype.ext $ (strict_mono_mul_left_of_pos a.2).injective $
+    by convert congr_arg subtype.val h,
+  le_of_mul_le_mul_left := λ a b c h, subtype.coe_le_coe.1 $ (mul_le_mul_left a.2).1 h,
+  .. subtype.linear_order _,
+  .. @positive.subtype.ordered_comm_monoid R
+    { mul_comm := is_commutative.comm, .. ‹linear_ordered_semiring R› } _  }
+
+end mul_comm
+
+end positive

src/data/pnat/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Neil Strickland
 -/
 import data.nat.basic
+import algebra.order.positive.ring
 
 /-!
 # The positive natural numbers
@@ -14,7 +15,8 @@ This file defines the type `ℕ+` or `pnat`, the subtype of natural numbers that
 /-- `ℕ+` is the type of positive natural numbers. It is defined as a subtype,
   and the VM representation of `ℕ+` is the same as `ℕ` because the proof
   is not stored. -/
-@[derive linear_order]
+@[derive [decidable_eq, add_left_cancel_semigroup, add_right_cancel_semigroup, add_comm_semigroup,
+  linear_ordered_cancel_comm_monoid, linear_order, has_add, has_mul, has_one, distrib]]
 def pnat := {n : ℕ // 0 < n}
 notation `ℕ+` := pnat
 
@@ -100,8 +102,6 @@ open nat
  subtraction, division and powers.
 -/
 
-instance : decidable_eq ℕ+ := λ (a b : ℕ+), by apply_instance
-
 @[simp] lemma mk_le_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
   (⟨n, hn⟩ : ℕ+) ≤ ⟨k, hk⟩ ↔ n ≤ k := iff.rfl
 
@@ -125,22 +125,17 @@ lemma coe_injective : function.injective (coe : ℕ+ → ℕ) := subtype.coe_inj
 
 @[simp] theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n := rfl
 
-instance : has_add ℕ+ := ⟨λ a b, ⟨(a  + b : ℕ), add_pos a.pos b.pos⟩⟩
-
-instance : add_comm_semigroup ℕ+ := coe_injective.add_comm_semigroup coe (λ _ _, rfl)
-
 @[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl
 
 /-- `pnat.coe` promoted to an `add_hom`, that is, a morphism which preserves addition. -/
 def coe_add_hom : add_hom ℕ+ ℕ :=
 { to_fun := coe,
   map_add' := add_coe }
 
-instance : add_left_cancel_semigroup ℕ+ :=
-coe_injective.add_left_cancel_semigroup coe (λ _ _, rfl)
-
-instance : add_right_cancel_semigroup ℕ+ :=
-coe_injective.add_right_cancel_semigroup coe (λ _ _, rfl)
+instance : covariant_class ℕ+ ℕ+ (+) (≤) := positive.covariant_class_add_le
+instance : covariant_class ℕ+ ℕ+ (+) (<) := positive.covariant_class_add_lt
+instance : contravariant_class ℕ+ ℕ+ (+) (≤) := positive.contravariant_class_add_le
+instance : contravariant_class ℕ+ ℕ+ (+) (<) := positive.contravariant_class_add_lt
 
 /-- An equivalence between `ℕ+` and `ℕ` given by `pnat.nat_pred` and `nat.succ_pnat`. -/
 @[simps { fully_applied := ff }] def _root_.equiv.pnat_equiv_nat : ℕ+ ≃ ℕ :=
@@ -157,22 +152,12 @@ coe_injective.add_right_cancel_semigroup coe (λ _ _, rfl)
 @[simp] lemma _root_.order_iso.pnat_iso_nat_symm_apply :
   ⇑order_iso.pnat_iso_nat.symm = nat.succ_pnat := rfl
 
-@[priority 10]
-instance : covariant_class ℕ+ ℕ+ ((+)) (≤) :=
-⟨by { rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, simp [←pnat.coe_le_coe] }⟩
-
 @[simp] theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 := n.2.ne'
 
 theorem to_pnat'_coe {n : ℕ} : 0 < n → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos
 
 @[simp] theorem coe_to_pnat' (n : ℕ+) : (n : ℕ).to_pnat' = n := eq (to_pnat'_coe n.pos)
 
-instance : has_mul ℕ+ := ⟨λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩⟩
-instance : has_one ℕ+ := ⟨succ_pnat 0⟩
-instance : has_pow ℕ+ ℕ := ⟨λ x n, ⟨x ^ n, pow_pos x.2 n⟩⟩
-
-instance : comm_monoid ℕ+ := coe_injective.comm_monoid coe rfl (λ _ _, rfl) (λ _ _, rfl)
-
 theorem lt_add_one_iff : ∀ {a b : ℕ+}, a < b + 1 ↔ a ≤ b :=
 λ a b, nat.lt_add_one_iff
 
@@ -223,8 +208,7 @@ def coe_monoid_hom : ℕ+ →* ℕ :=
 
 @[simp] lemma coe_coe_monoid_hom : (coe_monoid_hom : ℕ+ → ℕ) = coe := rfl
 
-@[simp]
-lemma coe_eq_one_iff {m : ℕ+} : (m : ℕ) = 1 ↔ m = 1 := by rw [← one_coe, coe_inj]
+@[simp] lemma coe_eq_one_iff {m : ℕ+} : (m : ℕ) = 1 ↔ m = 1 := subtype.coe_injective.eq_iff' one_coe
 
 @[simp] lemma le_one_iff {n : ℕ+} : n ≤ 1 ↔ n = 1 := le_bot_iff
 
@@ -238,17 +222,6 @@ lemma lt_add_right (n m : ℕ+) : n < n + m := (lt_add_left n m).trans_eq (add_c
 @[simp] theorem pow_coe (m : ℕ+) (n : ℕ) : ((m ^ n : ℕ+) : ℕ) = (m : ℕ) ^ n :=
 rfl
 
-instance : ordered_cancel_comm_monoid ℕ+ :=
-{ mul_le_mul_left := by { intros, apply nat.mul_le_mul_left, assumption },
-  le_of_mul_le_mul_left := by { intros a b c h, apply nat.le_of_mul_le_mul_left h a.property, },
-  mul_left_cancel := λ a b c h, by
- { replace h := congr_arg (coe : ℕ+ → ℕ) h,
-   exact eq ((nat.mul_right_inj a.pos).mp h)},
-  .. pnat.comm_monoid,
-  .. pnat.linear_order }
-
-instance : distrib ℕ+ := coe_injective.distrib coe (λ _ _, rfl) (λ _ _, rfl)
-
 /-- Subtraction a - b is defined in the obvious way when
   a > b, and by a - b = 1 if a ≤ b.
 -/