1 Ring of Integers of a Quadratic Field (Formalisation-Oriented)
Let \(d\) be an integer different from \(0\) and \(1\). We also assume that \(d\) is squarefree. We write \(K\) for the \(\mathbb {Q}\)-algebra generated by \(\sqrt{d}\): to be precise, we implement \(K\) using QuadraticAlgebra \(\mathbb {Q}\) d 0.
For all rational \(r\), we have \(r^2 \neq d\), so \(K\) is a field.
Clear since we assume that \(d\) is squarefree.
We have that \(d = \pm 1 \bmod 4\) or \(d = 2 \bmod 4\).
If \(d = 0 \bmod 4\) then \(d\) would not be squarefree.
We now write \(R\) for \(\mathbb {Z}[\sqrt{d}]\): we have that \(K\) is an \(R\)-algebra in the obvious way. Note that \(R\) is implemented as QuadraticAlgebra \(\mathbb {Z}\) d 0.
We have that \(\sqrt{d}\) is an integral element of \(K\).
Clear since \(\sqrt{d}\) is a root of \(x^2-d\).
Note that, in Lean, the above proposition technically says that the image in \(K\) of \(\sqrt{d}\) as element of \(R\) is integral.
1.1 Trace and norm
We fix in this section two rational numbers \(a, b \in \mathbb {Q}\) and we write \(z\) for \(a + b \sqrt{d} \in K\).
We have that \(z \in \mathbb {Q}\) if and only if \(b = 0\).
Clear.
If \(b \neq 0\) then the minimal polynomial of \(z\) over \(\mathbb {Q}\) is
It’s clear that \(z\) is a root of \(P\) and that \(P \in \mathbb {Q}[X]\) is monic. Irreducibility follows by the fact that \(P\) has a root that is irrational.
We have that the trace of \(z\) is \(2a\).
If \(b = 0\) then \(z = a \in \mathbb {Q}\) and the trace is \(2a\) since \([K : \mathbb {Q}] = 2\). Otherwise this is clear by Lemma 5.
We have that the norm of \(z\) is \(a^2-db^2\).
If \(b = 0\) then \(z = a \in \mathbb {Q}\) and the norm is \(a^2\) since \([K : \mathbb {Q}] = 2\). Otherwise this is clear by Lemma 5.
1.1.1 Integrality
We now suppose that \(z \in \mathcal{O}_K\).
We have that \(2a \in \mathbb {Z}\).
Since the trace of an algebraic integer is an integers, this follows by Lemma 6.
We write \(t\) (for trace) to denote \(2a\) as an integer. Mathematically we have \(t = 2a\).
We have that \(a^2-db^2 \in \mathbb {Z}\).
Since the norm of an algebraic integer is an integers, this follows by Lemma 7.
We write \(n\) (for norm) to denote \(a^2-db^2\) as an integer. Mathematically we have \(n = a^2-db^2\).
We have that \(4n = (2a)^2 - d(2b)^2\).
Obvious by applying 11.
Let \(n\) be a squarefree integer and let \(r\) be a rational such that \(b r^2\) is an integer. Then \(r\) is itself an integer.
Easy.
We have that \(2b \in \mathbb {Z}\).
We write \(B_2\) to denote \(2b\) as an integer. Mathematically we have \(B_2 = 2b\).
If \(a \in \mathbb {Z}\) then \(b \in \mathbb {Z}\).
If \(a\) is an integer, we write \(B\) to denote \(b\) as an integer. Mathematically we have \(B = b\).
If \(a \not\in \mathbb {Z}\) then \(d = 1 \bmod {4}\).
1.2 The case \(d \neq 1 \bmod {4}\)
Assume that \(d = 2 \bmod {4}\) or \(d = 3 \bmod {4}\). Then
By Lemma 3 we know that \(\mathbb {Z}[\sqrt{d}] \subseteq \mathcal{O}_K\). Let \(z = a + b \sqrt{d} \in \mathcal{O}_K\), with \(a, b \in \mathbb {Q}\). By Lemma 18 we have that \(a \in \mathbb {Z}\) (since by Lemma 2 we cannot have \(d = 1 \bmod {4}\)), and so by Lemma 16 we have \(b \in \mathbb {Z}\), so \(z \in \mathbb {Z}[\sqrt{d}]\).
1.3 The case \(d = 1 \bmod {4}\)
We assume in this section that \(d = 1 \bmod {4}\) and we write \(e = \frac{d-1}{4}\).
We have that \(e\) is an integer and \(4e = d - 1\).
Obvious.
We write \(S\) for the ring \(\mathbb {Z}\left[ \frac{1+\sqrt{d}}{2} \right]\), implemented as QuadraticAlgebra \(\mathbb {Z}\) e 1.
We have that
so that \(S\) is an \(R\)-algebra.
Obvious by Lemma 20.
We have that
so that \(K\) is an \(S\)-algebra.
Obvious by Lemma 20.
The obvious diagram between \(R\), \(S\) and \(K\) commutes.
Clear.
We have that \(\frac{1+\sqrt{d}}{2} \in \mathcal{O}_K\).
Clear since \(\frac{1+\sqrt{d}}{2}\) is a root of \(X^2 - X - e \in \mathbb {Z}[X]\).
Take \(z = a + b \sqrt{d} \in \mathcal{O}_K\) with \(a, b \in \mathbb {Q}\). If \(a \in \mathbb {Z}\) then \(z \in \mathbb {Z}\left[ \frac{1+\sqrt{d}}{2} \right]\).
By Lemma 16 we have that \(b \in \mathbb {Z}\) and so \(z \in \mathbb {Z}[\sqrt{d}] \subseteq \mathbb {Z}\left[ \frac{1+\sqrt{d}}{2} \right]\).
We have
By Lemma 24 we know that \(\mathbb {Z}\left[ \frac{1+\sqrt{d}}{2} \right] \subseteq \mathcal{O}_K\). Let \(z = a + b \sqrt{d} \in \mathcal{O}_K\), with \(a, b \in \mathbb {Q}\).
If \( a \in \mathbb {Z}\) we conclude by Lemma 25.
If \(a \notin \mathbb {Z}\), let us consider
\[ z' = z - \frac{1+\sqrt{d}}{2} = a - \frac{1}{2} + \left( b - \frac{1}{2} \right) \sqrt{d} \in \mathcal{O}_K \]Since \(2a \in \mathbb {Z}\) and \(a \notin \mathbb {Z}\), we have that \(a - \frac{1}{2} \in \mathbb {Z}\), so by Lemma 25, we have that \(z' \in \mathbb {Z}\left[ \frac{1+\sqrt{d}}{2} \right]\) and so \(z \in \mathbb {Z}\left[ \frac{1+\sqrt{d}}{2} \right]\).