3 The rationals
We can now define the rationals, starting with our copy of the integers \(\mathrm{MyInt}\).
We follow a similar path to the one for \(\mathrm{MyInt}\).
3.1 The prerationals
\(\mathrm{MyRat}\) will be a quotient of a type called \(\mathrm{MyPrerat}\).
Let \(\mathrm{MyPrerat}\) be \(\mathrm{MyInt}\times (\mathrm{MyInt}\setminus \{ 0\} )\).
We define a relation \(R\) on \(\mathrm{MyPrerat}\) as follows: \((a,b)\) and \((c, d)\) are related if and only if
\(R\) is a reflexive relation.
Exercise.
\(R\) is a symmetric relation.
Exercise.
\(R\) is a transitive relation.
Exercise.
We have that \(R\) is an equivalence relation. From now on, we will write \(x \approx y\) for \(x R y\).
We define an operation, called negation on \(\mathrm{MyPrerat}\) as follows: the negation of \(x = (a,b)\) is \((-a,b)\):
Note that it is automatically well defined (meaning that second component of \((-a,b)\) is different from \(0\)).
If \(x \approx x'\), then \(-x \approx -x'\).
Exercise.
We define an operation, called addition on \(\mathrm{MyPrerat}\) as follows: the addition of \(x = (a,b)\) and \(y = (c, d)\) is
Do you see why it is well defined?
If \(x \approx x'\) and \(y \approx y'\), then \(x + y \approx x' + y'\).
Exercise.
We define an operation, called multiplication on \(\mathrm{MyPrerat}\) as follows: the multiplication of \(x = (a,b)\) and \(y = (c, d)\) is
If \(x \approx x'\) and \(y \approx y'\), then \(x * y \approx x' * y'\).
Exercise.
We define an operation, called inversion on \(\mathrm{MyPrerat}\) as follows: the inverse of \(x = (a,b)\) is:
Note that \(x^{-1}\) is always defined!
If \(x \approx x'\), then \(x^{-1} \approx x'^{-1}\).
Exercise.
3.2 The rationals
3.2.1 Definitions
We define our rationals \(\mathrm{MyRat}\) as
We will write \(⟦ (a, b) ⟧\) for the class of \((a,b)\).
We define the zero of \(\mathrm{MyRat}\), denoted \(0\) as the class of \((0,1)\) (note that \(1 \neq 0\) in \(\mathrm{MyInt}\)).
We define the one of \(\mathrm{MyRat}\), denoted \(1\) as the class of \((1,1)\) (note that \(1 \neq 0\) in \(\mathrm{MyInt}\)).
3.2.2 Commutative ring structure
We define the negation of \(x = ⟦ (a, b) ⟧\) in \(\mathrm{MyRat}\) as
Thanks to Lemma 71 this is well defined.
We define the addition of \(x = ⟦ (a, b) ⟧\) and \(y = ⟦ (c, d) ⟧\) in \(\mathrm{MyRat}\) as
Thanks to Lemma 73 this is well defined.
We define the multiplication of \(x = ⟦ (a, b) ⟧\) and \(y = ⟦ (c, d) ⟧\) in \(\mathrm{MyRat}\) as
Thanks to Lemma 75 this is well defined.
We define the inverse of \(x = ⟦ (a, b) ⟧\) in \(\mathrm{MyRat}\) as
Thanks to Lemma 77 this is well defined.
\(\mathrm{MyRat}\) with addition and multiplication is a commutative ring.
We have to prove various properties, namely:
addition is associative
\(0\) works as neutral element for addition (on both sides)
existence of an inverse for addition (we prove that \(x + (-x) = (-x) + x = 0\))
addition is commutative
left and right distributivity of multiplication with respect to addition
associativity of multiplication
\(1\) works as neutral element for multiplication (on both sides)
All the proofs are essentially identical, going to \(\mathrm{MyInt}\), unravelling the definition and then checking the equality holds in \(\mathrm{MyInt}\).
In \(\mathrm{MyRat}\) we have \(0 \neq 1\).
If \(0 = 1\) by definition we would have \(⟦ (0,1) ⟧ = ⟦ (1,1) ⟧\) so \(0*1=1*0\) in \(\mathrm{MyInt}\), that is absurd.
Let \(x \neq 0\) be in \(\mathrm{MyRat}\). Then \(x * x^{-1} = 1\).
Let \(x = ⟦ (a,b) ⟧\), with \(b \neq 0\). Since \(x \neq 0\) we have \(a \neq 0\) and so \(x^{-1} = ⟦ (b,a) ⟧\). The lemma follows by definition of multiplication.
\(\mathrm{MyRat}\) with addition and multiplication is a field.
Clear because of Lemma 87.
3.2.3 The inclusion \(i \colon \mathrm{MyNat}\to \mathrm{MyRat}\)
We define a map
We have that \(i(0) = 0\).
Clear from the definition.
We have that \(i(1) = 1\).
Clear from the definition.
For all \(a\) and \(b\) in \(\mathrm{MyNat}\) we have that
We have \(i(a+b) = ⟦ (\mathrm{MyInt}.i (a+b), 1) ⟧ = ⟦ (\mathrm{MyInt}.i (a), 1) + (\mathrm{MyInt}.i (b), 1) ⟧\), \(i(a) = ⟦ (\mathrm{MyInt}.i(a), 1) ⟧\) and \(i(b) = ⟦ (\mathrm{MyInt}.i (b), 1) ⟧\), so we need to prove that
that is obvious from the definition.
For all \(a\) and \(b\) in \(\mathrm{MyNat}\) we have that
Similar to the proof of Lemma 92.
We have that \(i\) is injective.
Let \(a\) and \(b\) be such that \(i(a)=i(b)\). This means \(⟦ (\mathrm{MyInt}.i a,1) ⟧ = ⟦ (\mathrm{MyInt}.i b,1) ⟧\), so \((\mathrm{MyInt}.i a) * 1 = 1 * (\mathrm{MyInt}.i b)\). Hence \(\mathrm{MyInt}.i a = \mathrm{MyInt}.i b\), and injectivity of \(\mathrm{MyInt}.i\) gives \(a = b\).
3.2.4 The inclusion \(j \colon \mathrm{MyInt}\to \mathrm{MyRat}\)
We define a map
We have that \(j(0) = 0\).
Clear from the definition.
We have that \(j(1) = 1\).
Clear from the definition.
For all \(a\) and \(b\) in \(\mathrm{MyInt}\) we have that
Exercise.
For all \(a\) and \(b\) in \(\mathrm{MyInt}\) we have that
Exercise.
We have that \(j\) is injective.
Exercise.
Let \(n\) be a natural number. Then \(\mathrm{MyRat}.j (\mathrm{MyInt}.i (n)) = \mathrm{MyRat}.i (n)\).
It follows from unravelling all the definitions.
Let \(a\) and \(b\) be in \(\mathrm{MyInt}\) with \(b \neq 0\). Then \(⟦ (a, b) ⟧ = j(a)*j(b)^{-1}\).
Exercise.
3.2.5 Nonnegativity
Before defining the order on \(\mathrm{MyRat}\), let’s define the notion of nonnegativity.
Given \(x\) in \(\mathrm{MyRat}\), we say that \(x\) is nonnegative if it has a representative with nonnegative numerator and positive denominator: there exist \(a\) and \(b\) in \(\mathrm{MyInt}\) with \(0 \leq a\) and \(0 {\lt} b\) such that
This is the usual condition \(0 \leq a/b\) after choosing a positive denominator.
We have that \(0\) in \(\mathrm{MyRat}\) is nonnegative.
Obvious.
We have that \(1\) in \(\mathrm{MyRat}\) is nonnegative.
Obvious.
Let \(x\) be in \(\mathrm{MyRat}\) such that both \(x\) and \(-x\) are nonnegative. Then \(x = 0\).
Unravelling all the definitions we end up with \(a\), \(b\), \(c\) and \(d\) in \(\mathrm{MyInt}\) such that \(0 \leq a\), \(0 {\lt} b\), \(0 \leq c\), \(0 {\lt} d\) and \(-(a*d)=b*c\). This implies \(a=0\).
Let \(x\) be in \(\mathrm{MyRat}\) such that \(x\) is not nonnegative. Then \(-x\) is nonnegative.
Annoying but easy, left as an exercise.
Let \(x\) and \(y\) be in \(\mathrm{MyRat}\) both nonnegative. Then \(x+y\) is nonnegative.
Exercise.
Let \(x\) and \(y\) be in \(\mathrm{MyRat}\) both nonnegative. Then \(x*y\) is nonnegative.
Exercise.
Let \(x\) be in \(\mathrm{MyRat}\) be nonnegative. Then \(x^{-1}\) is nonnegative.
Exercise.
3.2.6 The order
Let \(x\) and \(y\) in \(\mathrm{MyRat}\). We write \(x \leq y\) if \(y - x\) is nonnegative.
We have that \(0 \leq x\) if and only if \(x\) is nonnegative.
Clear.
In \(\mathrm{MyRat}\) we have that \(0 \leq 1\).
Clear because of Lemma 105.
The relation \(\leq \) on \(\mathrm{MyRat}\) is reflexive.
Clear because of Lemma 104.
The relation \(\leq \) on \(\mathrm{MyRat}\) is transitive.
It follows from Lemma 108.
The relation \(\leq \) on \(\mathrm{MyRat}\) is antisymmetric.
It follows from Lemma 106.
It follows that \(\leq \) is an order relation.
3.2.7 Interaction between the order and the ring structure
Let \(x\), \(y\) and \(z\) in \(\mathrm{MyRat}\) be such that \(x \leq y\). Then \(x + z \leq y + z\).
Clear from the definitions.
Let \(x\) and \(y\) in \(\mathrm{MyRat}\) be such that \(0 \leq x\) and \(0 \leq y\). Then \(0 \leq x * y\).
It follows from Lemma 109.
We have proved that \(\mathrm{MyRat}\) is an ordered ring.
3.2.8 Interaction between the order and the inclusions
Let \(x\) and \(y\) in \(\mathrm{MyInt}\). We have that \(j(x) \leq j(y)\) if and only if \(x \leq y\).
Exercise.
Let \(x\) and \(y\) in \(\mathrm{MyNat}\). We have that \(i(x) \leq i(y)\) if and only if \(x \leq y\).
3.2.9 The linear order structure
The order \(\leq \) on \(\mathrm{MyRat}\) is a total order.
This follows by Lemma 107.
We have that \(\mathrm{MyRat}\) with \(\leq \) is a linear order
Clear from the lemma above.
Let \(x\) and \(y\) in \(\mathrm{MyRat}\) be such that \(0 {\lt} x\) and \(0 {\lt} y\). Then \(0 {\lt} x * y\).
Exercise.
We now have that \(\mathrm{MyRat}\) is a strict ordered ring: a nontrivial ring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.
For every \(x\) in \(\mathrm{MyRat}\) there exists \(n\) in \(\mathrm{MyNat}\) such that \(x \leq i(n)\).
Choose a representative \(x = a/b\) with \(0 {\lt} b\). By Lemma 63, choose a natural number \(n\) such that \(a \leq \mathrm{MyInt}.i(n)\). Since \(b\) is positive and \(\mathrm{MyInt}.i(n)\) is nonnegative, we have \(\mathrm{MyInt}.i(n) \leq b \cdot \mathrm{MyInt}.i(n)\). Thus \(a \leq b \cdot \mathrm{MyInt}.i(n)\), which is exactly \(a/b \leq n\), hence \(x \leq i(n)\).