Ring extensions of ℚ and rational modules (UniMath#1452)

This PR aims to fill some gaps in ring-theoretical relations between ℤ
and ℚ:

- `rational-ℤ` is the initial ring homomorphism `ℤ → ℚ`;
- elements of `ℤ⁺` are invertible in `ℚ`;
- any ring homomorphism `ℚ → R` inverts positive integers;
- misc. elementary algebraic properties;

We also introduce the following concepts:

- **ring extensions of ℚ**: rings `R` such that the image of `ℤ⁺` by the
initial ring homomorphism `ℤ → R` consists of invertible elements; with
the following results:
  
- the initial ring homomorphism `ι : ℤ → R` into a ring extensions of ℚ
extends to a map `ℚ → R` by
    ```γ : p/q ↦ (ι p)(ι q)⁻¹```;
- any ring that admits a ring homomorphism `f : ℚ → R` is a **ring
extensions of ℚ** and `f` is homotopic to `γ`;
    - all ring homomorphisms `ℚ → R` are equal;
- a ring is a **ring extensions of ℚ** if and only if there exists some
ring homomorphism `ℚ → R`.
    - `ℚ` is a rational ring;
- the rational extension `γ : p/q ↦ (ι p)(ι q)⁻¹` of the initial ring
homomorphism `ι : ℤ → R` into a **ring extensions of ℚ** is a ring
homomorphism `ℚ → R` ;
    - `ℚ` is the initial **ring extensions of ℚ**;
    - `ℚ` is the localization of `ℤ` at `ℤ⁺`.

- **rational modules**: Abelian groups whose ring of endomorphisms are
**ring extensions of ℚ**. It is equivalent to the type of left/right
modules over the ring of rational numbers, i.e., rational vector spaces.

---------

Co-authored-by: Garrett Figueroa <garrett.figueroa@gmail.com>

Author: malarbol

src/elementary-number-theory.lagda.md

@@ -165,6 +165,7 @@ open import elementary-number-theory.relatively-prime-integers public
 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-extension-rational-numbers-of-rational-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

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

@@ -11,6 +11,7 @@ module elementary-number-theory.additive-group-of-rational-numbers where
 ```agda
 open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.group-of-integers
 open import elementary-number-theory.rational-numbers
 
 open import foundation.dependent-pair-types
@@ -21,6 +22,7 @@ open import foundation.universe-levels
 open import group-theory.abelian-groups
 open import group-theory.commutative-monoids
 open import group-theory.groups
+open import group-theory.homomorphisms-abelian-groups
 open import group-theory.monoids
 open import group-theory.semigroups
 ```
@@ -99,3 +101,10 @@ abstract
   left-swap-add-ℚ : (p q r : ℚ) → p +ℚ (q +ℚ r) ＝ q +ℚ (p +ℚ r)
   left-swap-add-ℚ = left-swap-add-Ab abelian-group-add-ℚ
 ```
+
+### The inclusion of integers in the rationals is an additive homomorphism
+
+```agda
+hom-add-rational-ℤ : hom-Ab ℤ-Ab abelian-group-add-ℚ
+hom-add-rational-ℤ = (rational-ℤ , λ {x y} → inv (add-rational-ℤ x y))
+```

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

@@ -452,6 +452,46 @@ abstract
       ＝ q +ℚ q by ap-add-ℚ (left-unit-law-mul-ℚ q) (left-unit-law-mul-ℚ q)
 ```
 
+### The product of a rational number and its denominator is its numerator
+
+```agda
+module _
+  (x : ℚ)
+  where
+
+  opaque
+    unfolding mul-ℚ
+
+    eq-numerator-mul-denominator-ℚ :
+      mul-ℚ
+        ( x)
+        ( rational-ℤ (denominator-ℚ x)) ＝
+      rational-ℤ (numerator-ℚ x)
+    eq-numerator-mul-denominator-ℚ =
+      ( eq-ℚ-sim-fraction-ℤ
+        ( mul-fraction-ℤ
+          ( fraction-ℚ x)
+          ( in-fraction-ℤ (denominator-ℚ x)))
+        ( in-fraction-ℤ (numerator-ℚ x))
+        ( associative-mul-ℤ
+          ( numerator-ℚ x)
+          ( denominator-ℚ x)
+          ( one-ℤ))) ∙
+      ( is-retraction-rational-fraction-ℚ
+        ( rational-ℤ (numerator-ℚ x)))
+
+    eq-numerator-mul-denominator-ℚ' :
+      mul-ℚ
+        ( rational-ℤ (denominator-ℚ x))
+        ( x) ＝
+      rational-ℤ (numerator-ℚ x)
+    eq-numerator-mul-denominator-ℚ' =
+      ( commutative-mul-ℚ
+        ( rational-ℤ (denominator-ℚ x))
+        ( x)) ∙
+      ( eq-numerator-mul-denominator-ℚ)
+```
+
 ## See also
 
 - The multiplicative monoid structure on the rational numbers is defined in

src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md

@@ -160,3 +160,24 @@ abstract
       ( y)
       ( commutative-mul-ℚ⁺ x y)
 ```
+
+### Inversion on the positive rational numbers interchanges numerator and denominator
+
+```agda
+module _
+  (x : ℚ⁺)
+  where
+
+  opaque
+    unfolding inv-ℚ⁺
+
+    eq-numerator-inv-denominator-ℚ⁺ :
+      numerator-ℚ⁺ (inv-ℚ⁺ x) ＝ denominator-ℚ⁺ x
+    eq-numerator-inv-denominator-ℚ⁺ =
+      ind-Σ eq-numerator-inv-denominator-is-positive-ℚ x
+
+    eq-denominator-inv-numerator-ℚ⁺ :
+      denominator-ℚ⁺ (inv-ℚ⁺ x) ＝ numerator-ℚ⁺ x
+    eq-denominator-inv-numerator-ℚ⁺ =
+      ind-Σ eq-denominator-inv-numerator-is-positive-ℚ x
+```

src/elementary-number-theory/positive-integers.lagda.md

@@ -98,6 +98,9 @@ module _
 ```agda
 one-positive-ℤ : positive-ℤ
 one-positive-ℤ = (one-ℤ , star)
+
+one-ℤ⁺ : ℤ⁺
+one-ℤ⁺ = one-positive-ℤ
 ```
 
 ## Properties
@@ -156,6 +159,27 @@ is-positive-int-is-nonzero-ℕ (succ-ℕ x) H = star
 
 positive-int-ℕ⁺ : ℕ⁺ → positive-ℤ
 positive-int-ℕ⁺ (n , n≠0) = int-ℕ n , is-positive-int-is-nonzero-ℕ n n≠0
+
+positive-nat-ℤ⁺ : positive-ℤ → ℕ⁺
+positive-nat-ℤ⁺ (inr (inr x) , k>0) = succ-nonzero-ℕ' x
+
+abstract
+  is-section-positive-nat-ℤ⁺ :
+    (k : ℤ⁺) → positive-int-ℕ⁺ (positive-nat-ℤ⁺ k) ＝ k
+  is-section-positive-nat-ℤ⁺ (inr (inr k) , k>0) =
+    eq-type-subtype subtype-positive-ℤ refl
+
+  is-retraction-positive-nat-ℤ⁺ :
+    (n : ℕ⁺) → positive-nat-ℤ⁺ (positive-int-ℕ⁺ n) ＝ n
+  is-retraction-positive-nat-ℤ⁺ (zero-ℕ , n≠0) = ex-falso (n≠0 refl)
+  is-retraction-positive-nat-ℤ⁺ (succ-ℕ n , n≠0) = eq-nonzero-ℕ refl
+
+  is-equiv-positive-int-ℕ⁺ : is-equiv positive-int-ℕ⁺
+  is-equiv-positive-int-ℕ⁺ =
+    is-equiv-is-invertible
+      ( positive-nat-ℤ⁺)
+      ( is-section-positive-nat-ℤ⁺)
+      ( is-retraction-positive-nat-ℤ⁺)
 ```
 
 ### The canonical equivalence between natural numbers and positive integers

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

@@ -174,6 +174,9 @@ abstract
 positive-rational-positive-ℤ : positive-ℤ → ℚ⁺
 positive-rational-positive-ℤ (z , pos-z) = rational-ℤ z , pos-z
 
+positive-rational-ℤ⁺ : ℤ⁺ → ℚ⁺
+positive-rational-ℤ⁺ = positive-rational-positive-ℤ
+
 one-ℚ⁺ : ℚ⁺
 one-ℚ⁺ = (one-ℚ , is-positive-int-positive-ℤ one-positive-ℤ)
 ```
@@ -504,6 +507,14 @@ module _
     right-inverse-law-mul-is-positive-ℚ =
       (commutative-mul-ℚ x _) ∙ (left-inverse-law-mul-is-positive-ℚ)
 
+    eq-numerator-inv-denominator-is-positive-ℚ :
+      numerator-ℚ (inv-is-positive-ℚ) ＝ denominator-ℚ x
+    eq-numerator-inv-denominator-is-positive-ℚ = refl
+
+    eq-denominator-inv-numerator-is-positive-ℚ :
+      denominator-ℚ (inv-is-positive-ℚ) ＝ numerator-ℚ x
+    eq-denominator-inv-numerator-is-positive-ℚ = refl
+
   is-mul-invertible-is-positive-ℚ : is-invertible-element-Monoid monoid-mul-ℚ x
   pr1 is-mul-invertible-is-positive-ℚ = inv-is-positive-ℚ
   pr1 (pr2 is-mul-invertible-is-positive-ℚ) =

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

@@ -0,0 +1,103 @@
+# The ring extension of rational numbers of the ring of rational numbers
+
+```agda
+module elementary-number-theory.ring-extension-rational-numbers-of-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.positive-integers
+open import elementary-number-theory.ring-of-integers
+open import elementary-number-theory.ring-of-rational-numbers
+
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.logical-equivalences
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import ring-theory.homomorphisms-ring-extensions-rational-numbers
+open import ring-theory.homomorphisms-rings
+open import ring-theory.localizations-rings
+open import ring-theory.ring-extensions-rational-numbers
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+The
+[ring of rational numbers](elementary-number-theory.ring-of-rational-numbers.md)
+is a [ring extension of `ℚ`](ring-theory.ring-extensions-rational-numbers.md) so
+`ℚ` is the initial ring extension of `ℚ`: the type of
+[ring homomorphisms](ring-theory.homomorphisms-rings.md) from `ℚ` to a ring
+extension of `ℚ` is [contractible](foundation-core.contractible-types.md).
+
+As a corollary, `ℚ` is the [localization](ring-theory.localizations-rings.md) of
+`ℤ` at `ℤ⁺`: any ring homomorphism `ℤ → R` that inverts the positive integers
+extends to a ring homomorphism `ℚ → R`.
+
+## Definition
+
+### `ℚ` is a rational extension of itself
+
+```agda
+is-rational-extension-ring-ℚ : is-rational-extension-Ring ring-ℚ
+is-rational-extension-ring-ℚ =
+  is-rational-extension-has-rational-hom-Ring
+    ( ring-ℚ)
+    ( id-hom-Ring ring-ℚ)
+
+rational-extension-ring-ℚ : Rational-Extension-Ring lzero
+rational-extension-ring-ℚ =
+  ( ring-ℚ , is-rational-extension-ring-ℚ)
+```
+
+## Properties
+
+### The ring of rational numbers is the initial ring extension of `ℚ`
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-initial-rational-extension-ring-ℚ :
+    (R : Rational-Extension-Ring l) →
+    is-contr (hom-Rational-Extension-Ring rational-extension-ring-ℚ R)
+  is-initial-rational-extension-ring-ℚ R =
+    is-contr-rational-hom-Rational-Extension-Ring R
+```
+
+### The ring of rational numbers is the localization of the ring of integers at `ℤ⁺`
+
+```agda
+module _
+  {l : Level}
+  where
+
+  universal-property-localization-positive-integers-ring-ℚ :
+    universal-property-localization-subset-Ring
+      ( l)
+      ( ℤ-Ring)
+      ( ring-ℚ)
+      ( subtype-positive-ℤ)
+      ( initial-hom-Ring ring-ℚ)
+      ( is-rational-extension-ring-ℚ)
+  universal-property-localization-positive-integers-ring-ℚ T =
+    is-equiv-has-converse-is-prop
+      ( is-prop-has-rational-hom-Ring T)
+      ( is-prop-type-subtype
+        ( inverts-subset-prop-hom-Ring ℤ-Ring T subtype-positive-ℤ)
+        ( is-prop-is-contr (is-initial-ℤ-Ring T)))
+      ( λ (f , H) →
+        initial-hom-Rational-Extension-Ring
+          ( ( T) ,
+            ( inv-tr
+              ( inverts-subset-hom-Ring ℤ-Ring T subtype-positive-ℤ)
+              ( contraction-initial-hom-Ring T f)
+              ( H))))
+```

src/elementary-number-theory/ring-of-integers.lagda.md

@@ -203,3 +203,27 @@ compute-integer-multiple-ℤ-Ring k l =
       by
       integer-multiple-one-ℤ-Ring _
 ```
+
+### The image of `ℤ` in a ring is commutative
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  abstract
+    is-commutative-map-initial-hom-Ring :
+      (p q : ℤ) →
+      mul-Ring
+        ( R)
+        ( map-initial-hom-Ring R p)
+        ( map-initial-hom-Ring R q) ＝
+      mul-Ring
+        ( R)
+        ( map-initial-hom-Ring R q)
+        ( map-initial-hom-Ring R p)
+    is-commutative-map-initial-hom-Ring p q =
+      ( inv (preserves-mul-initial-hom-Ring R p q)) ∙
+      ( ap (map-initial-hom-Ring R) (commutative-mul-ℤ p q)) ∙
+      ( preserves-mul-initial-hom-Ring R q p)
+```

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

@@ -14,14 +14,22 @@ open import commutative-algebra.commutative-rings
 open import elementary-number-theory.additive-group-of-rational-numbers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.multiplicative-monoid-of-rational-numbers
+open import elementary-number-theory.positive-integers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.ring-of-integers
+open import elementary-number-theory.unit-fractions-rational-numbers
 
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
 open import foundation.unital-binary-operations
 open import foundation.universe-levels
 
 open import group-theory.semigroups
 
+open import ring-theory.homomorphisms-rings
+open import ring-theory.localizations-rings
 open import ring-theory.rings
 ```
 
@@ -64,3 +72,69 @@ commutative-ring-ℚ : Commutative-Ring lzero
 pr1 commutative-ring-ℚ = ring-ℚ
 pr2 commutative-ring-ℚ = commutative-mul-ℚ
 ```
+
+### The inclusion of integers in the rationals is the initial ring homomorphism
+
+```agda
+hom-ring-rational-ℤ : hom-Ring ℤ-Ring ring-ℚ
+hom-ring-rational-ℤ =
+  ( hom-add-rational-ℤ) ,
+  ( λ {x y} → inv (mul-rational-ℤ x y)) ,
+  ( refl)
+
+abstract
+  htpy-map-initial-hom-ring-rational-ℤ :
+    map-initial-hom-Ring ring-ℚ ~ rational-ℤ
+  htpy-map-initial-hom-ring-rational-ℤ =
+    htpy-initial-hom-Ring ring-ℚ hom-ring-rational-ℤ
+
+  eq-initial-hom-ring-rational-ℤ : initial-hom-Ring ring-ℚ ＝ hom-ring-rational-ℤ
+  eq-initial-hom-ring-rational-ℤ =
+    contraction-initial-hom-Ring ring-ℚ hom-ring-rational-ℤ
+```
+
+### The positive integers are invertible in ℚ
+
+```agda
+abstract
+  inverts-positive-integers-rational-ℤ :
+    inverts-subset-hom-Ring
+      ( ℤ-Ring)
+      ( ring-ℚ)
+      ( subtype-positive-ℤ)
+      ( hom-ring-rational-ℤ)
+  inverts-positive-integers-rational-ℤ k k>0 =
+    ( reciprocal-rational-ℤ⁺ (k , k>0)) ,
+    ( right-inverse-law-reciprocal-rational-ℤ⁺ (k , k>0) ,
+      left-inverse-law-reciprocal-rational-ℤ⁺ (k , k>0))
+```
+
+### Any ring homomorphism from ℚ inverts the positive integers
+
+```agda
+module _
+  {l : Level} (R : Ring l) (f : hom-Ring ring-ℚ R)
+  where
+
+  abstract
+    inverts-positive-integers-rational-hom-Ring :
+      inverts-subset-hom-Ring
+        ( ℤ-Ring)
+        ( R)
+        ( subtype-positive-ℤ)
+        ( comp-hom-Ring ℤ-Ring ring-ℚ R f hom-ring-rational-ℤ)
+    inverts-positive-integers-rational-hom-Ring k k>0 =
+      preserves-invertible-elements-hom-Ring
+        ( ring-ℚ)
+        ( R)
+        ( f)
+        ( inverts-positive-integers-rational-ℤ k k>0)
+```
+
+## See also
+
+- [`ring-extension-rational-numbers-of-rational-numbers`](elementary-number-theory.ring-extension-rational-numbers-of-rational-numbers.md):
+  the trivial
+  [ring extension of `ℚ`](ring-theory.ring-extensions-rational-numbers.md) where
+  it is proven that `ℚ` is the
+  [localization](ring-theory.localizations-rings.md) of `ℤ` at `ℤ⁺`.