2 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}\).
2.1 The prerationals
\(\mathrm{MyRat}\) will be a quotient of a type called \(\mathrm{MyPrerat}\).
Let \(\mathrm{MyPrerat}\) be \(\mathrm{MyInt}\times \mathrm{MyInt}\backslash \{ 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.
Exercice.
\(R\) is a symmetric relation.
Exercice.
\(R\) is a transitive relation.
Exercice.
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'\).
Exercice.
We define an operation, called addition on \(\mathrm{MyPrerat}\) as follows: the addition of \(x = (a,b)\) and \(y = (b, c)\) is
Do you see why it is well defined?
If \(x \approx x'\) and \(y \approx y'\), then \(x + y \approx x' + y'\).
Exercice.
We define an operation, called multiplication on \(\mathrm{MyPrerat}\) as follows: the multiplication of \(x = (a,b)\) and \(y = (b, c)\) is
If \(x \approx x'\) and \(y \approx y'\), then \(x * y \approx x' * y'\).
Exercice.
We define an operation, called negation 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}\).
Exercice.
2.2 The rationals
2.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}\)).
2.2.2 Commutative ring structure
We define the negation of \(x = ⟦ (a, b) ⟧\) in \(\mathrm{MyInt}\) as
Thanks to Lemma 47 this is well defined.
We define the addition of \(x = ⟦ (a, b) ⟧\) and \(y = ⟦ (c, d) ⟧\) in \(\mathrm{MyInt}\) as
Thanks to Lemma 49 this is well defined.
We define the multiplication of \(x = ⟦ (a, b) ⟧\) and \(y = ⟦ (c, d) ⟧\) in \(\mathrm{MyInt}\) as
Thanks to Lemma 51 this is well defined.
We define the negation of \(x = ⟦ (a, b) ⟧\) in \(\mathrm{MyInt}\) as
Thanks to Lemma 53 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 63.
2.2.3 The inclusion \(i \colon \mathbb {N}\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 \(\mathbb {N}\) 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 \(\mathbb {N}\) we have that
Similar to the proof of Lemma 68.
We have that \(i\) is injective.
Let \(a\) be such that \(i(a)=0\). This means \(⟦ (\mathrm{MyInt}.i a,1) ⟧ = ⟦ (0,1) ⟧\) so \((\mathrm{MyInt}.i a) * 1 = 1 * 0\) and hence \(\mathrm{MyInt}.i a = 0\) so \(a = 0\).
2.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
Exercice.
For all \(a\) and \(b\) in \(\mathbb {N}\) we have that
Exercice.
We have that \(j\) is injective.
Exercice.
Let \(n\) be a natural number. Then \(\mathrm{MyRat}.j (\mathrm{MyInt}.i (n)) = 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}\).
Exercice.
2.2.5 Nonegativity
Before defining the order on \(\mathrm{MyRat}\), let’s define the notion of nonnegativity.
Given \(x = (a,b)\) in \(\mathrm{MyRat}\), we say that \(x\) is nonnegative if \(0 \leq a\) and \(0 {\lt} b\).
Can you see why it corresponds to the “usual definition” when we think that \(x = a/b\)?
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 exercice.
Let \(x\) and \(y\) be in \(\mathrm{MyRat}\) both nonnegative. Then \(x+y\) is nonnegative.
Exercice.
Let \(x\) and \(y\) be in \(\mathrm{MyRat}\) both nonnegative. Then \(x*y\) is nonnegative.
Exercice.
Let \(x\) be in \(\mathrm{MyRat}\) be nonnegative. Then \(x^{-1}\) is nonnegative.
Exercice.
2.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 81.
The relation \(\leq \) on \(\mathrm{MyRat}\) is reflexive.
Clear because of Lemma 80.
The relation \(\leq \) on \(\mathrm{MyRat}\) is transitive.
It follows from Lemma 84.
The relation \(\leq \) on \(\mathrm{MyRat}\) is antisymmetric.
It follows from Lemma 82.
It follows that \(\leq \) is an order relation.
2.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 \(z + x ≤ z + y\).
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 85.
We have proved that \(\mathrm{MyRat}\) is an ordered ring.
2.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\).
Exercice.
Let \(x\) and \(y\) in \(\mathbb {N}\). We have that \(i(x) \leq i(y)\) if and only if \(x \leq y\).
2.2.9 The linear order structure
The order \(\leq \) on \(\mathrm{MyRat}\) is a total order.
This follows by Lemma 83.
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\).
Exercice.
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.