The commutative ring of rational numbers

src/elementary-number-theory.lagda.md

@@ -123,6 +123,7 @@ open import elementary-number-theory.relatively-prime-natural-numbers public
 open import elementary-number-theory.repeating-element-standard-finite-type public
 open import elementary-number-theory.retracts-of-natural-numbers public
 open import elementary-number-theory.ring-of-integers public
+open import elementary-number-theory.ring-of-rational-numbers public
 open import elementary-number-theory.sieve-of-eratosthenes public
 open import elementary-number-theory.square-free-natural-numbers public
 open import elementary-number-theory.squares-integers public

src/elementary-number-theory/multiplication-integer-fractions.lagda.md

@@ -7,11 +7,15 @@ module elementary-number-theory.multiplication-integer-fractions where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-integer-fractions
+open import elementary-number-theory.addition-integers
 open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integers
 open import elementary-number-theory.multiplication-positive-and-negative-integers
 
 open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 ```
@@ -108,3 +112,38 @@ commutative-mul-fraction-ℤ :
 commutative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) =
   ap-mul-ℤ (commutative-mul-ℤ nx ny) (commutative-mul-ℤ dy dx)
 ```
+
+### Multiplication on integer fractions distributes on the left over addition
+
+```agda
+left-distributive-mul-add-fraction-ℤ :
+  (x y z : fraction-ℤ) →
+  sim-fraction-ℤ
+    (mul-fraction-ℤ x (add-fraction-ℤ y z))
+    (add-fraction-ℤ (mul-fraction-ℤ x y) (mul-fraction-ℤ x z))
+left-distributive-mul-add-fraction-ℤ
+  (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) =
+    ( ap
+      ( ( nx *ℤ (ny *ℤ dz +ℤ nz *ℤ dy)) *ℤ_)
+      ( ( interchange-law-mul-mul-ℤ dx dy dx dz) ∙
+        ( associative-mul-ℤ dx dx (dy *ℤ dz)))) ∙
+    ( interchange-law-mul-mul-ℤ
+      ( nx)
+      ( ny *ℤ dz +ℤ nz *ℤ dy)
+      ( dx)
+      ( dx *ℤ (dy *ℤ dz))) ∙
+    ( inv
+      ( associative-mul-ℤ
+        ( nx *ℤ dx)
+        ( ny *ℤ dz +ℤ nz *ℤ dy)
+        ( dx *ℤ (dy *ℤ dz)))) ∙
+    ( ap
+      ( _*ℤ (dx *ℤ (dy *ℤ dz)))
+      ( ( left-distributive-mul-add-ℤ
+          ( nx *ℤ dx)
+          ( ny *ℤ dz)
+          ( nz *ℤ dy)) ∙
+        ( ap-add-ℤ
+          ( interchange-law-mul-mul-ℤ nx dx ny dz))
+          ( interchange-law-mul-mul-ℤ nx dx nz dy)))
+```

src/elementary-number-theory/multiplication-rational-numbers.lagda.md

@@ -11,6 +11,7 @@ module elementary-number-theory.multiplication-rational-numbers where
 ```agda
 open import elementary-number-theory.addition-integer-fractions
 open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.greatest-common-divisor-integers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
@@ -44,12 +45,70 @@ rational numbers.
 mul-ℚ : ℚ → ℚ → ℚ
 mul-ℚ (x , p) (y , q) = rational-fraction-ℤ (mul-fraction-ℤ x y)
 
+mul-ℚ' : ℚ → ℚ → ℚ
+mul-ℚ' x y = mul-ℚ y x
+
 infixl 40 _*ℚ_
 _*ℚ_ = mul-ℚ
 ```
 
 ## Properties
 
+### The multiplication of a rational number by zero is zero
+
+```agda
+module _
+  (x : ℚ)
+  where
+
+  left-zero-law-mul-ℚ : zero-ℚ *ℚ x ＝ zero-ℚ
+  left-zero-law-mul-ℚ =
+    ( eq-ℚ-sim-fraction-ℤ
+      ( mul-fraction-ℤ (fraction-ℚ zero-ℚ) (fraction-ℚ x))
+      ( fraction-ℚ zero-ℚ)
+      ( eq-is-zero-ℤ
+        ( ap (mul-ℤ' one-ℤ) (left-zero-law-mul-ℤ (numerator-ℚ x)))
+        ( left-zero-law-mul-ℤ _))) ∙
+    ( is-retraction-rational-fraction-ℚ zero-ℚ)
+
+  right-zero-law-mul-ℚ : x *ℚ zero-ℚ ＝ zero-ℚ
+  right-zero-law-mul-ℚ =
+    ( eq-ℚ-sim-fraction-ℤ
+      ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ zero-ℚ))
+      ( fraction-ℚ zero-ℚ)
+      ( eq-is-zero-ℤ
+        ( ap (mul-ℤ' one-ℤ) (right-zero-law-mul-ℤ (numerator-ℚ x)))
+        ( left-zero-law-mul-ℤ _))) ∙
+    ( is-retraction-rational-fraction-ℚ zero-ℚ)
+```
+
+### If the product of two rational numbers is zero, the left or right factor is zero
+
+```agda
+is-zero-is-zero-mul-ℚ :
+  (x y : ℚ) → is-zero-ℚ (x *ℚ y) → (is-zero-ℚ x) + (is-zero-ℚ y)
+is-zero-is-zero-mul-ℚ x y H =
+  rec-coproduct
+    ( inl ∘ is-zero-is-zero-numerator-ℚ x)
+    ( inr ∘ is-zero-is-zero-numerator-ℚ y)
+    ( is-zero-is-zero-mul-ℤ
+      ( numerator-ℚ x)
+      ( numerator-ℚ y)
+      ( ( inv
+          ( eq-reduce-numerator-fraction-ℤ
+            ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)))) ∙
+        ( ap
+          ( mul-ℤ'
+            ( gcd-ℤ
+              ( numerator-ℚ x *ℤ numerator-ℚ y)
+              ( denominator-ℚ x *ℤ denominator-ℚ y)))
+          ( ( is-zero-numerator-is-zero-ℚ (x *ℚ y) H) ∙
+            ( left-zero-law-mul-ℤ
+              ( gcd-ℤ
+                (numerator-ℚ x *ℤ numerator-ℚ y)
+                (denominator-ℚ x *ℤ denominator-ℚ y)))))))
+```
+
 ### Unit laws for multiplication on rational numbers
 
 ```agda
@@ -179,4 +238,78 @@ negative-law-mul-ℚ x y =
   ( left-negative-law-mul-ℚ x (neg-ℚ y)) ∙
   ( ap neg-ℚ (right-negative-law-mul-ℚ x y)) ∙
   ( neg-neg-ℚ (x *ℚ y))
+
+swap-neg-mul-ℚ : (x y : ℚ) → x *ℚ (neg-ℚ y) ＝ (neg-ℚ x) *ℚ y
+swap-neg-mul-ℚ x y =
+  ( right-negative-law-mul-ℚ x y) ∙
+  ( inv (left-negative-law-mul-ℚ x y))
+```
+
+### Multiplication on rational numbers distributes over addition
+
+```agda
+left-distributive-mul-add-ℚ :
+  (x y z : ℚ) → x *ℚ (y +ℚ z) ＝ x *ℚ y +ℚ x *ℚ z
+left-distributive-mul-add-ℚ x y z =
+  eq-ℚ-sim-fraction-ℤ
+    ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z)))
+    ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z)))
+    ( transitive-sim-fraction-ℤ
+      ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z)))
+      ( mul-fraction-ℤ
+        ( fraction-ℚ x)
+        ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
+      ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z)))
+      ( transitive-sim-fraction-ℤ
+        ( mul-fraction-ℤ
+          ( fraction-ℚ x)
+          ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
+        ( add-fraction-ℤ
+          ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
+          ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z)))
+        ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z)))
+        ( sim-fraction-add-fraction-ℤ
+          ( sim-reduced-fraction-ℤ
+            ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)))
+          ( sim-reduced-fraction-ℤ
+            ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z))))
+        ( left-distributive-mul-add-fraction-ℤ
+          ( fraction-ℚ x)
+          ( fraction-ℚ y)
+          ( fraction-ℚ z)))
+      ( sim-fraction-mul-fraction-ℤ
+        ( refl-sim-fraction-ℤ (fraction-ℚ x))
+        ( transitive-sim-fraction-ℤ
+          ( fraction-ℚ (y +ℚ z))
+          ( reduce-fraction-ℤ (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
+          ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))
+          ( symmetric-sim-fraction-ℤ
+            ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))
+            ( reduce-fraction-ℤ (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))
+            ( sim-reduced-fraction-ℤ
+              (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))))
+          ( refl-sim-fraction-ℤ (fraction-ℚ (y +ℚ z))))))
+
+right-distributive-mul-add-ℚ :
+  (x y z : ℚ) → (x +ℚ y) *ℚ z ＝ x *ℚ z +ℚ y *ℚ z
+right-distributive-mul-add-ℚ x y z =
+  ( commutative-mul-ℚ (x +ℚ y) z) ∙
+  ( left-distributive-mul-add-ℚ z x y) ∙
+  ( ap-add-ℚ (commutative-mul-ℚ z x) (commutative-mul-ℚ z y))
+```
+
+### Multiplication on rational numbers distributes over the difference
+
+```agda
+left-distributive-mul-diff-ℚ :
+  (z x y : ℚ) → z *ℚ (x -ℚ y) ＝ (z *ℚ x) -ℚ (z *ℚ y)
+left-distributive-mul-diff-ℚ z x y =
+  ( left-distributive-mul-add-ℚ z x (neg-ℚ y)) ∙
+  ( ap ((z *ℚ x) +ℚ_) (right-negative-law-mul-ℚ z y))
+
+right-distributive-mul-diff-ℚ :
+  (x y z : ℚ) → (x -ℚ y) *ℚ z ＝ (x *ℚ z) -ℚ (y *ℚ z)
+right-distributive-mul-diff-ℚ x y z =
+  ( right-distributive-mul-add-ℚ x (neg-ℚ y) z) ∙
+  ( ap ((x *ℚ z) +ℚ_) (left-negative-law-mul-ℚ y z))
 ```

src/elementary-number-theory/ring-of-rational-numbers.lagda.md

@@ -0,0 +1,56 @@
+# The ring of rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.ring-of-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.group-of-rational-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+The
+[commutative group of rational numbers](elementary-number-theory.group-of-rational-numbers.md)
+equipped with
+[multiplication](elementary-number-theory.multiplication-rational-numbers.md) is
+a [commutative](commutative-algebra.commutative-rings.md)
+[ring](ring-theory.rings.md).
+
+## Definitions
+
+### The commutative ring of rational numbers
+
+```agda
+ℚ-Ring : Ring lzero
+pr1 ℚ-Ring = ℚ-Ab
+pr1 (pr1 (pr2 ℚ-Ring)) = mul-ℚ
+pr2 (pr1 (pr2 ℚ-Ring)) = associative-mul-ℚ
+pr1 (pr1 (pr2 (pr2 ℚ-Ring))) = one-ℚ
+pr1 (pr2 (pr1 (pr2 (pr2 ℚ-Ring)))) = left-unit-law-mul-ℚ
+pr2 (pr2 (pr1 (pr2 (pr2 ℚ-Ring)))) = right-unit-law-mul-ℚ
+pr1 (pr2 (pr2 (pr2 ℚ-Ring))) = left-distributive-mul-add-ℚ
+pr2 (pr2 (pr2 (pr2 ℚ-Ring))) = right-distributive-mul-add-ℚ
+
+ℚ-Commutative-Ring : Commutative-Ring lzero
+pr1 ℚ-Commutative-Ring = ℚ-Ring
+pr2 ℚ-Commutative-Ring = commutative-mul-ℚ
+```