feat: NNRat.cast (#11203)

Define the canonical coercion from the nonnegative rationals to any division semiring.

From LeanAPAP

Author: YaelDillies

Mathlib/Algebra/DirectLimit.lean

@@ -1011,6 +1011,7 @@ protected noncomputable def field [DirectedSystem G fun i j h => f' i j h] :
   inv := inv G fun i j h => f' i j h
   mul_inv_cancel := fun p => DirectLimit.mul_inv_cancel G fun i j h => f' i j h
   inv_zero := dif_pos rfl
+  nnqsmul := _
   qsmul := _
 #align field.direct_limit.field Field.DirectLimit.field
 

Mathlib/Algebra/Field/Basic.lean

@@ -268,6 +268,7 @@ noncomputable def DivisionRing.ofIsUnitOrEqZero [Ring R] (h : ∀ a : R, IsUnit
     DivisionRing R where
   toRing := ‹Ring R›
   __ := groupWithZeroOfIsUnitOrEqZero h
+  nnqsmul := _
   qsmul := _
 #align division_ring_of_is_unit_or_eq_zero DivisionRing.ofIsUnitOrEqZero
 
@@ -282,20 +283,23 @@ noncomputable def Field.ofIsUnitOrEqZero [CommRing R] (h : ∀ a : R, IsUnit a 
 end NoncomputableDefs
 
 namespace Function.Injective
-variable [Zero α] [Add α] [Neg α] [Sub α] [One α] [Mul α] [Inv α] [Div α] [SMul ℕ α]
-  [SMul ℤ α] [SMul ℚ α] [Pow α ℕ] [Pow α ℤ] [NatCast α] [IntCast α] [RatCast α]
+variable [Zero α] [Add α] [Neg α] [Sub α] [One α] [Mul α] [Inv α] [Div α] [SMul ℕ α] [SMul ℤ α]
+  [SMul ℚ≥0 α] [SMul ℚ α] [Pow α ℕ] [Pow α ℤ] [NatCast α] [IntCast α] [NNRatCast α] [RatCast α]
   (f : α → β) (hf : Injective f)
 
 /-- Pullback a `DivisionSemiring` along an injective function. -/
 @[reducible] -- See note [reducible non-instances]
 protected def divisionSemiring [DivisionSemiring β] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
-    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (natCast : ∀ n : ℕ, f n = n) : DivisionSemiring α where
+    (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : DivisionSemiring α where
   toSemiring := hf.semiring f zero one add mul nsmul npow natCast
   __ := hf.groupWithZero f zero one mul inv div npow zpow
+  nnratCast_def q := hf $ by rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
+  nnqsmul := (· • ·)
+  nnqsmul_def q a := hf $ by rw [nnqsmul, NNRat.smul_def, mul, nnratCast]
 #align function.injective.division_semiring Function.Injective.divisionSemiring
 
 /-- Pullback a `DivisionSemiring` along an injective function. -/
@@ -304,14 +308,14 @@ protected def divisionRing [DivisionRing β] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
     (div : ∀ x y, f (x / y) = f x / f y)
-    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
+    (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n)
+    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q)
     (ratCast : ∀ q : ℚ, f q = q) : DivisionRing α where
   toRing := hf.ring f zero one add mul neg sub nsmul zsmul npow natCast intCast
   __ := hf.groupWithZero f zero one mul inv div npow zpow
-  __ := hf.divisionSemiring f zero one add mul inv div nsmul npow zpow natCast
+  __ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
   ratCast_def q := hf $ by erw [ratCast, div, intCast, natCast, Rat.cast_def]
   qsmul := (· • ·)
   qsmul_def q a := hf $ by erw [qsmul, mul, Rat.smul_def, ratCast]
@@ -322,12 +326,12 @@ protected def divisionRing [DivisionRing β] (zero : f 0 = 0) (one : f 1 = 1)
 protected def semifield [Semifield β] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
-    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (natCast : ∀ n : ℕ, f n = n) : Semifield α where
+    (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : Semifield α where
   toCommSemiring := hf.commSemiring f zero one add mul nsmul npow natCast
   __ := hf.commGroupWithZero f zero one mul inv div npow zpow
-  __ := hf.divisionSemiring f zero one add mul inv div nsmul npow zpow natCast
+  __ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
 #align function.injective.semifield Function.Injective.semifield
 
 /-- Pullback a `Field` along an injective function. -/
@@ -336,15 +340,15 @@ protected def field [Field β] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
     (div : ∀ x y, f (x / y) = f x / f y)
-    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
-    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
+    (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n)
+    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q)
     (ratCast : ∀ q : ℚ, f q = q) :
     Field α where
   toCommRing := hf.commRing f zero one add mul neg sub nsmul zsmul npow natCast intCast
-  __ := hf.divisionRing f zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow
-    natCast intCast ratCast
+  __ := hf.divisionRing f zero one add mul neg sub inv div nsmul zsmul nnqsmul qsmul npow zpow
+    natCast intCast nnratCast ratCast
 #align function.injective.field Function.Injective.field
 
 end Function.Injective

Mathlib/Algebra/Field/Defs.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
+Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro, Yaël Dillies
 -/
 import Mathlib.Algebra.Ring.Defs
 import Mathlib.Data.Rat.Init
@@ -59,6 +59,14 @@ universe u
 
 variable {α β K : Type*}
 
+/-- The default definition of the coercion `ℚ≥0 → K` for a division semiring `K`.
+
+`↑q : K` is defined as `(q.num : K) / (q.den : K)`.
+
+Do not use this directly (instances of `DivisionSemiring` are allowed to override that default for
+better definitional properties). Instead, use the coercion. -/
+def NNRat.castRec [NatCast K] [Div K] (q : ℚ≥0) : K := q.num / q.den
+
 /-- The default definition of the coercion `ℚ → K` for a division ring `K`.
 
 `↑q : K` is defined as `(q.num : K) / (q.den : K)`.
@@ -79,7 +87,23 @@ itself). See also note [forgetful inheritance].
 
 If the division semiring has positive characteristic `p`, our division by zero convention forces
 `nnratCast (1 / p) = 1 / 0 = 0`. -/
-class DivisionSemiring (α : Type*) extends Semiring α, GroupWithZero α where
+class DivisionSemiring (α : Type*) extends Semiring α, GroupWithZero α, NNRatCast α where
+  protected nnratCast := NNRat.castRec
+  /-- However `NNRat.cast` is defined, it must be propositionally equal to `a / b`.
+
+  Do not use this lemma directly. Use `NNRat.cast_def` instead. -/
+  protected nnratCast_def (q : ℚ≥0) : (NNRat.cast q : α) = q.num / q.den := by intros; rfl
+  /-- Scalar multiplication by a nonnegative rational number.
+
+  Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
+  `nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.
+
+  Do not use directly. Instead use the `•` notation. -/
+  protected nnqsmul : ℚ≥0 → α → α
+  /-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.
+
+  Do not use this lemma directly. Use `NNRat.smul_def` instead. -/
+  protected nnqsmul_def (q : ℚ≥0) (a : α) : nnqsmul q a = NNRat.cast q * a := by intros; rfl
 #align division_semiring DivisionSemiring
 
 /-- A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.
@@ -93,11 +117,27 @@ See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ
 If the division ring has positive characteristic `p`, our division by zero convention forces
 `ratCast (1 / p) = 1 / 0 = 0`. -/
 class DivisionRing (α : Type*)
-  extends Ring α, DivInvMonoid α, Nontrivial α, RatCast α where
+  extends Ring α, DivInvMonoid α, Nontrivial α, NNRatCast α, RatCast α where
   /-- For a nonzero `a`, `a⁻¹` is a right multiplicative inverse. -/
   protected mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
   /-- The inverse of `0` is `0` by convention. -/
   protected inv_zero : (0 : α)⁻¹ = 0
+  protected nnratCast := NNRat.castRec
+  /-- However `NNRat.cast` is defined, it must be equal to `a / b`.
+
+  Do not use this lemma directly. Use `NNRat.cast_def` instead. -/
+  protected nnratCast_def (q : ℚ≥0) : (NNRat.cast q : α) = q.num / q.den := by intros; rfl
+  /-- Scalar multiplication by a nonnegative rational number.
+
+  Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
+  `nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.
+
+  Do not use directly. Instead use the `•` notation. -/
+  protected nnqsmul : ℚ≥0 → α → α
+  /-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.
+
+  Do not use this lemma directly. Use `NNRat.smul_def` instead. -/
+  protected nnqsmul_def (q : ℚ≥0) (a : α) : nnqsmul q a = NNRat.cast q * a := by intros; rfl
   protected ratCast := Rat.castRec
   /-- However `Rat.cast q` is defined, it must be propositionally equal to `q.num / q.den`.
 
@@ -150,6 +190,20 @@ class Field (K : Type u) extends CommRing K, DivisionRing K
 instance (priority := 100) Field.toSemifield [Field α] : Semifield α := { ‹Field α› with }
 #align field.to_semifield Field.toSemifield
 
+namespace NNRat
+variable [DivisionSemiring α]
+
+instance (priority := 100) smulDivisionSemiring : SMul ℚ≥0 α := ⟨DivisionSemiring.nnqsmul⟩
+
+lemma cast_def (q : ℚ≥0) : (q : α) = q.num / q.den := DivisionSemiring.nnratCast_def _
+lemma smul_def (q : ℚ≥0) (a : α) : q • a = q * a := DivisionSemiring.nnqsmul_def q a
+
+variable (α)
+
+@[simp] lemma smul_one_eq_coe (q : ℚ≥0) : q • (1 : α) = q := by rw [NNRat.smul_def, mul_one]
+
+end NNRat
+
 namespace Rat
 variable [DivisionRing K] {a b : K}
 

Mathlib/Algebra/Field/IsField.lean

@@ -69,6 +69,7 @@ noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R)
   inv a := if ha : a = 0 then 0 else Classical.choose (h.mul_inv_cancel ha)
   inv_zero := dif_pos rfl
   mul_inv_cancel a ha := by convert Classical.choose_spec (h.mul_inv_cancel ha); exact dif_neg ha
+  nnqsmul := _
 #align is_field.to_semifield IsField.toSemifield
 
 /-- Transferring from `IsField` to `Field`. -/

Mathlib/Algebra/Field/MinimalAxioms.lean

@@ -42,4 +42,5 @@ def Field.ofMinimalAxioms (K : Type u)
   { exists_pair_ne := exists_pair_ne
     mul_inv_cancel := mul_inv_cancel
     inv_zero := inv_zero
+    nnqsmul := _
     qsmul := _ }

Mathlib/Algebra/Field/Opposite.lean

@@ -17,23 +17,31 @@ variable {α : Type*}
 
 namespace MulOpposite
 
+@[to_additive] instance instNNRatCast [NNRatCast α] : NNRatCast αᵐᵒᵖ := ⟨fun q ↦ op q⟩
 @[to_additive] instance instRatCast [RatCast α] : RatCast αᵐᵒᵖ := ⟨fun q ↦ op q⟩
 
 @[to_additive (attr := simp, norm_cast)]
-theorem op_ratCast [RatCast α] (q : ℚ) : op (q : α) = q :=
-  rfl
+lemma op_nnratCast [NNRatCast α] (q : ℚ≥0) : op (q : α) = q := rfl
+
+@[to_additive (attr := simp, norm_cast)]
+lemma unop_nnratCast [NNRatCast α] (q : ℚ≥0) : unop (q : αᵐᵒᵖ) = q := rfl
+
+@[to_additive (attr := simp, norm_cast)]
+lemma op_ratCast [RatCast α] (q : ℚ) : op (q : α) = q := rfl
 #align mul_opposite.op_rat_cast MulOpposite.op_ratCast
 #align add_opposite.op_rat_cast AddOpposite.op_ratCast
 
 @[to_additive (attr := simp, norm_cast)]
-theorem unop_ratCast [RatCast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q :=
-  rfl
+lemma unop_ratCast [RatCast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q := rfl
 #align mul_opposite.unop_rat_cast MulOpposite.unop_ratCast
 #align add_opposite.unop_rat_cast AddOpposite.unop_ratCast
 
 instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ where
   __ := instSemiring
   __ := instGroupWithZero
+  nnqsmul := _
+  nnratCast_def q := unop_injective $ by rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
+    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
 
 instance instDivisionRing [DivisionRing α] : DivisionRing αᵐᵒᵖ where
   __ := instRing
@@ -57,6 +65,9 @@ namespace AddOpposite
 instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ where
   __ := instSemiring
   __ := instGroupWithZero
+  nnqsmul := _
+  nnratCast_def q := unop_injective $ by rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
+    NNRat.cast_def, div_eq_mul_inv]
 
 instance instDivisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ where
   __ := instRing

Mathlib/Algebra/Field/ULift.lean

@@ -21,8 +21,11 @@ variable {α : Type u} {x y : ULift.{v} α}
 
 namespace ULift
 
+instance instNNRatCast [NNRatCast α] : NNRatCast (ULift α) where nnratCast q := up q
 instance instRatCast [RatCast α] : RatCast (ULift α) where ratCast q := up q
 
+@[simp, norm_cast] lemma up_nnratCast [NNRatCast α] (q : ℚ≥0) : up (q : α) = q := rfl
+@[simp, norm_cast] lemma down_nnratCast [NNRatCast α] (q : ℚ≥0) : down (q : ULift α) = q := rfl
 @[simp, norm_cast] lemma up_ratCast [RatCast α] (q : ℚ) : up (q : α) = q := rfl
 @[simp, norm_cast] lemma down_ratCast [RatCast α] (q : ℚ) : down (q : ULift α) = q := rfl
 #align ulift.up_rat_cast ULift.up_ratCast

Mathlib/Algebra/Module/Basic.lean

@@ -482,11 +482,6 @@ theorem map_rat_smul [AddCommGroup M] [AddCommGroup M₂]
   map_ratCast_smul f ℚ ℚ c x
 #align map_rat_smul map_rat_smul
 
-
-/-- A `Module` over `ℚ` restricts to a `Module` over `ℚ≥0`. -/
-instance [AddCommMonoid α] [Module ℚ α] : Module NNRat α :=
-  Module.compHom α NNRat.coeHom
-
 /-- There can be at most one `Module ℚ E` structure on an additive commutative group. -/
 instance subsingleton_rat_module (E : Type*) [AddCommGroup E] : Subsingleton (Module ℚ E) :=
   ⟨fun P Q => (Module.ext' P Q) fun r x =>

Mathlib/Algebra/Order/Archimedean.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Algebra.Order.Field.Power
 import Mathlib.Data.Int.LeastGreatest
 import Mathlib.Data.Rat.Floor

Mathlib/Algebra/Order/CauSeq/Completion.lean

@@ -203,8 +203,10 @@ section
 variable {α : Type*} [LinearOrderedField α]
 variable {β : Type*} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv]
 
+instance instNNRatCast : NNRatCast (Cauchy abv) where nnratCast q := ofRat q
 instance instRatCast : RatCast (Cauchy abv) where ratCast q := ofRat q
 
+@[simp, norm_cast] lemma ofRat_nnratCast (q : ℚ≥0) : ofRat (q : β) = (q : Cauchy abv) := rfl
 @[simp, norm_cast] lemma ofRat_ratCast (q : ℚ) : ofRat (q : β) = (q : Cauchy abv) := rfl
 #align cau_seq.completion.of_rat_rat_cast CauSeq.Completion.ofRat_ratCast
 
@@ -272,8 +274,11 @@ noncomputable instance Cauchy.divisionRing : DivisionRing (Cauchy abv) where
   exists_pair_ne := ⟨0, 1, zero_ne_one⟩
   inv_zero := inv_zero
   mul_inv_cancel x := CauSeq.Completion.mul_inv_cancel
+  nnqsmul := (· • ·)
   qsmul := (· • ·)
+  nnratCast_def q := by simp_rw [← ofRat_nnratCast, NNRat.cast_def, ofRat_div, ofRat_natCast]
   ratCast_def q := by rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]
+  nnqsmul_def q x := Quotient.inductionOn x fun f ↦ congr_arg mk <| ext fun i ↦ NNRat.smul_def _ _
   qsmul_def q x := Quotient.inductionOn x fun f ↦ congr_arg mk <| ext fun i ↦ Rat.smul_def _ _
 
 /-- Show the first 10 items of a representative of this equivalence class of cauchy sequences.