Multiplication on the rational numbers (#675)

This PR pulled the changes from #661 and prepared them for merge with
the library.

---------

Co-authored-by: Julian KG <juliankg@Julians-MacBook-Pro.local>

.gitignore

@@ -1,3 +1,6 @@
+# envrc
+\.envrc
+\.direnv/
 
 ### Agda ###
 *.agdai

src/elementary-number-theory.lagda.md

@@ -10,7 +10,7 @@ open import elementary-number-theory.ackermann-function public
 open import elementary-number-theory.addition-integer-fractions public
 open import elementary-number-theory.addition-integers public
 open import elementary-number-theory.addition-natural-numbers public
-open import elementary-number-theory.addition-rationals public
+open import elementary-number-theory.addition-rational-numbers public
 open import elementary-number-theory.arithmetic-functions public
 open import elementary-number-theory.based-induction-natural-numbers public
 open import elementary-number-theory.based-strong-induction-natural-numbers public
@@ -77,9 +77,11 @@ open import elementary-number-theory.modular-arithmetic public
 open import elementary-number-theory.modular-arithmetic-standard-finite-types public
 open import elementary-number-theory.monoid-of-natural-numbers-with-addition public
 open import elementary-number-theory.monoid-of-natural-numbers-with-maximum public
+open import elementary-number-theory.multiplication-integer-fractions public
 open import elementary-number-theory.multiplication-integers public
 open import elementary-number-theory.multiplication-lists-of-natural-numbers public
 open import elementary-number-theory.multiplication-natural-numbers public
+open import elementary-number-theory.multiplication-rational-numbers public
 open import elementary-number-theory.multiset-coefficients public
 open import elementary-number-theory.natural-numbers public
 open import elementary-number-theory.nonzero-natural-numbers public

src/elementary-number-theory/addition-rationals.lagda.md → src/elementary-number-theory/addition-rational-numbers.lagda.md

@@ -1,9 +1,9 @@
-# Addition on the rationals
+# Addition on the rational numbers
 
 ```agda
 {-# OPTIONS --lossy-unification #-}
 
-module elementary-number-theory.addition-rationals where
+module elementary-number-theory.addition-rational-numbers where
 ```
 
 <details><summary>Imports</summary>

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

@@ -0,0 +1,112 @@
+# Multiplication on integer fractions
+
+```agda
+module elementary-number-theory.multiplication-integer-fractions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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 foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+```
+
+</details>
+
+## Idea
+
+**Multiplication on integer fractions** is an extension of the
+[multiplicative operation](elementary-number-theory.multiplication-integers.md)
+on the [integers](elementary-number-theory.integers.md) to
+[integer fractions](elementary-number-theory.integer-fractions.md). Note that
+the basic properties of multiplication on integer fraction only hold up to
+fraction similarity.
+
+## Definition
+
+```agda
+mul-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ
+pr1 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos)) =
+  m *ℤ m'
+pr1 (pr2 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
+  n *ℤ n'
+pr2 (pr2 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
+  is-positive-mul-ℤ n-pos n'-pos
+
+mul-fraction-ℤ' : fraction-ℤ → fraction-ℤ → fraction-ℤ
+mul-fraction-ℤ' x y = mul-fraction-ℤ y x
+
+infix 30 _*fraction-ℤ_
+_*fraction-ℤ_ = mul-fraction-ℤ
+
+ap-mul-fraction-ℤ :
+  {x y x' y' : fraction-ℤ} → x ＝ x' → y ＝ y' →
+  x *fraction-ℤ y ＝ x' *fraction-ℤ y'
+ap-mul-fraction-ℤ p q = ap-binary mul-fraction-ℤ p q
+```
+
+## Properties
+
+### Multiplication respects the similarity relation
+
+```agda
+sim-fraction-mul-fraction-ℤ :
+  {x x' y y' : fraction-ℤ} →
+  sim-fraction-ℤ x x' →
+  sim-fraction-ℤ y y' →
+  sim-fraction-ℤ (x *fraction-ℤ y) (x' *fraction-ℤ y')
+sim-fraction-mul-fraction-ℤ
+  {(nx , dx , dxp)} {(nx' , dx' , dx'p)}
+  {(ny , dy , dyp)} {(ny' , dy' , dy'p)} p q =
+  equational-reasoning
+    (nx *ℤ ny) *ℤ (dx' *ℤ dy')
+    ＝ (nx *ℤ dx') *ℤ (ny *ℤ dy')
+      by interchange-law-mul-mul-ℤ nx ny dx' dy'
+    ＝ (nx' *ℤ dx) *ℤ (ny' *ℤ dy)
+      by ap-mul-ℤ p q
+    ＝ (nx' *ℤ ny') *ℤ (dx *ℤ dy)
+      by interchange-law-mul-mul-ℤ nx' dx ny' dy
+```
+
+### Unit laws
+
+```agda
+left-unit-law-mul-fraction-ℤ :
+  (k : fraction-ℤ) →
+  sim-fraction-ℤ (mul-fraction-ℤ one-fraction-ℤ k) k
+left-unit-law-mul-fraction-ℤ k = refl
+
+right-unit-law-mul-fraction-ℤ :
+  (k : fraction-ℤ) →
+  sim-fraction-ℤ (mul-fraction-ℤ k one-fraction-ℤ) k
+right-unit-law-mul-fraction-ℤ (n , d , p) =
+  ap-mul-ℤ (right-unit-law-mul-ℤ n) (inv (right-unit-law-mul-ℤ d))
+```
+
+### Multiplication is associative
+
+```agda
+associative-mul-fraction-ℤ :
+  (x y z : fraction-ℤ) →
+  sim-fraction-ℤ
+    (mul-fraction-ℤ (mul-fraction-ℤ x y) z)
+    (mul-fraction-ℤ x (mul-fraction-ℤ y z))
+associative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) =
+  ap-mul-ℤ (associative-mul-ℤ nx ny nz) (inv (associative-mul-ℤ dx dy dz))
+```
+
+### Multiplication is commutative
+
+```agda
+commutative-mul-fraction-ℤ :
+  (x y : fraction-ℤ) → sim-fraction-ℤ (x *fraction-ℤ y) (y *fraction-ℤ x)
+commutative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) =
+  ap-mul-ℤ (commutative-mul-ℤ nx ny) (commutative-mul-ℤ dy dx)
+```

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

@@ -0,0 +1,63 @@
+# Multiplication on the rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.multiplication-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.reduced-integer-fractions
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+```
+
+</details>
+
+## Idea
+
+**Multiplication** on the
+[rational numbers](elementary-number-theory.rational-numbers.md) is defined by
+extending
+[multiplication](elementary-number-theory.multiplication-integer-fractions.md)
+on [integer fractions](elementary-number-theory.integer-fractions.md) to the
+rational numbers.
+
+## Definition
+
+```agda
+mul-ℚ : ℚ → ℚ → ℚ
+mul-ℚ (x , p) (y , q) = in-fraction-ℤ (mul-fraction-ℤ x y)
+
+infix 30 _*ℚ_
+_*ℚ_ = mul-ℚ
+```
+
+## Properties
+
+### Unit laws
+
+```agda
+left-unit-law-mul-ℚ : (x : ℚ) → one-ℚ *ℚ x ＝ x
+left-unit-law-mul-ℚ x =
+  ( eq-ℚ-sim-fractions-ℤ
+    ( mul-fraction-ℤ one-fraction-ℤ (fraction-ℚ x))
+    ( fraction-ℚ x)
+    ( left-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙
+  ( in-fraction-fraction-ℚ x)
+
+right-unit-law-mul-ℚ : (x : ℚ) → x *ℚ one-ℚ ＝ x
+right-unit-law-mul-ℚ x =
+  ( eq-ℚ-sim-fractions-ℤ
+    ( mul-fraction-ℤ (fraction-ℚ x) one-fraction-ℤ)
+    ( fraction-ℚ x)
+    ( right-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙
+  ( in-fraction-fraction-ℚ x)
+```