3 Quadratic Forms over \(\mathbb {Q}\) and \(\mathbb {Q}_p\)
3.1 Quadratic Forms
The following definition is available in Mathlibunder the name QuadraticForm:
Let \(M\) be a module over a commutative ring \(A\). A function \(f : M \to A\) is called a quadratic form on \(M\) if
\(f(ax) = a^2f(x)\) for all \(a \in A, x \in M\),
The function \((x, y) \mapsto f(x + y) - f(x) - f(y)\) is a bilinear form.
The QuadraticForm folder of Mathlibcontains definitions and results about quadratic forms, including the bilinear map
associated to a quadratic form (see QuadraticMap.associated) and the definition and characterization of nondegenerate quadratic forms (see QuadraticMap.Nondegenerate).
A quadratic form \(f : M \to A\) is called isotropic if there exists a nonzero \(x \in M\) such that \(f(x) = 0\).
Let \(R\) be a commutative ring, let \(V\) be an \(R\)-module and let \(Q\) be a quadratic form on \(V\). We say that \(Q\) represents an element \(r \in R\) if there exists \(x \in V\) such that \(Q(v) = r\) and \(v \ne 0\).
Let \(R\) be a commutative ring, let \(V\) be an \(R\)-module and let \(Q\) be a quadratic form on \(V\). Then \(Q\) represents \(0\) if and only if it is isotropic.
This follows immediately from the definitions.
Let \(Q\) and \(Q'\) be two equivalent quadratic forms over \(R\) and let \(r \in \). Then \(Q\) represents \(r\) if and only if \(Q'\) represents \(r\). In particular, \(Q\) is isotropic if and only if \(Q'\) is isotropic.
By Lemma 3.1.4, it suffices to prove the first claim, which follows from the definition of equivalence of quadratic forms.
3.1.1 Orthogonal basis
Let \(K\) be a field in which \(2\) is invertible and let \(V\) be a \(K\)-vector space.
The definition of orthogonal basis for \(V\) is available in Mathlibas LinearMap.IsOrtho\(_i\). The lemma LinearMap.BilinForm.exists_orthogonal_basis proves that for any symmetric bilinear form \(B\) on \(V\) there exists an orthogonal basis with respect to \(B\).
Two bases of \(V\) are called contiguous if they have an element in common.
Let \(V\) be a \(K\)-vector space of dimension at least \(3\), let \(Q\) be a nondegenerate quadratic form on \(V\), and let \(b, b'\) be two \(Q\)-orthogonal bases of \(V\). Then there exists a finite sequence \((b^{(0)}, \cdots , b^{(m)})\) of orthogonal bases of \(V\) such that \(b^{(0)} = b\), \(b^{(m)} = b'\) and \(b^{(i)}\) is contiguous with \(b^{(i + 1)}\) for \(0 \le i {\lt} m\).
See [ .
A sequence of bases \((b^{(0)} = b, \cdots , b^{(m)} = b')\) as in Theorem 3.1.7 is called a chain of orthogonal bases contiguously relating \(b\) to \(b'\).
Let \(V\) be a \(K\)-vector space of dimension at least \(3\), let \(Q\) be a nondegenerate quadratic form on \(V\), and let \(b, b'\) be two \(Q\)-orthogonal bases of \(V\). Assume that
There exists \(x \in K\) such that \(b_x := b_1' + x b_2'\) is nonisotropic and generates with \(b_1\) a nondegenerate plane.
See [ .
3.1.2 Translations
Let \(R\) be a commutative ring, let \(V\) and \(W\) be \(R\)-modules and let \(Q\) and \(Q'\) be quadratic forms on \(V\) and \(W\), respectively. Then \(Q \dotplus Q'\) denotes the quadratic form on \(V \times W\) obtained by applying \(Q\) on \(V\) and \(Q'\) on \(W\). This is available in Mathlibas QuadraticMap.prod. Similarly, \(Q \dotminus Q'\) denotes the form \(Q \dotplus (-Q')\) on \(V \times W\).
A quadratic form is hyperbolic if it is equivalent to the form \(X^2 - Y^2\).
The quadratic form \(XY\) is hyperbolic.
TODO.
Let \(R\) be a commutative ring. If a quadratic form \(Q\) on an \(R\)-module \(V\) represents \(0\) and is nondegenerate, then \(Q\) is equivalent to \(H + Q'\), where \(H\) is hyperbolic. Moreover, \(f\) represents all elements of \(R\).
Fix \(x \in V\) such that \(Q(x) = 0\). Since \(Q\) is nondegenerate, there exists \(z \in V\) such that \(x \cdot z = 1\). The element \(y = 2z - (z\cdot z)x\) is isotropic and \(x \cdot y = 2\). The restriction of \(Q\) to the submodule \(U := Rx \oplus Ry\) is the desired hyperbolic form \(H\).
Let \(K\) be a field, let \(r \in K^\times \) and let \(Q\) be a quadratic form on a free \(K\)-vector space \(V\). Then \(Q\) represents \(r\) if and only if the form \(Q' := Q \dotminus rZ\) represents \(0\).
The forward implication is clear. For the second one, fix a basis for \(V\) and assume that \(Q' := Q \dotminus rZ\) has a nontrivial zero \((x_1, \cdots , x_n, z) \in V \times K\). Then either \(z = 0\), in which case \(Q\) represents zero and thus also \(r\), or \(Q(x_1/z, \cdots , x_n/z) = r\).
Let \(K\) be a field and \(Q\) and \(Q'\) be nondegenerate quadratic forms over \(K\) of rank at least \(1\). Then the following properties are equivalent:
\(Q \dotminus Q'\) represents \(0\).
There exists \(r \in K^\times \) which is represented by \(Q\) and \(Q'\).
There exists \(r \in K^\times \) such that \(Q \dotminus rZ^2\) and \(Q' \dotminus rZ^2\) represent \(0\).
The equivalence (b) \(\iff \) (c) follows from Corollary 3.1.13. The implication (b) \(\implies \) (a) is trivial. To show (a) \(\implies (b)\), write a nontrivial zero of \(Q \dotminus Q'\) in the form \((x, y)\) with \(Q(x) = Q'(y)\). If \(Q(x) \ne 0\), we are done. If \(Q(x) = 0\), then \(Q\) represents \(0\) and thus by Proposition 3.1.12 also all elements of \(K\). In particular, it represents all nonzero values taken by \(Q'\).
3.2 Quadratic Forms over \(\mathbb {Q}_p\)
Let \(p\) be a prime number and let \(f\) be a quadratic form of rank \(n\) over \(\mathbb {Q}_p\). Take a diagonal quadratic form \(a_1X_1^2 + \cdots + a_nX_n^2\) which is equivalent to \(f\); then the discriminant of \(f\) is the element \(d(f) = a_1 \cdots a_n \in \mathbb {Q}_p^\times /{\mathbb {Q}_p^\times }^2\).
Note that Mathlibcontains QuadraticForm.discr, as an element of \(\mathbb {Q}_p\). We might need to adjust some statements and proofs if we really need to regard it as an element in \(\mathbb {Q}_p^\times /{\mathbb {Q}_p^\times }^2\).
Let \(p\) be a prime number and let \(f\) be a quadratic form of rank \(n\) over \(\mathbb {Q}_p\). Take a diagonal quadratic form \(a_1X_1^2 + \cdots + a_nX_n^2\) which is equivalent to \(f\); then the Hasse–Minkowski invariant of \(f\) is the element
The value \(\epsilon (f)\) does not depend on the choice of diagonal quadratic form equivalent to \(f\).
Let \(b = (b_1, \cdots , b_n)\) be an orthogonal basis for \(V\) such that \(Q(x) = a_1 x_1^2 + \cdots + a_n x_n^2\) for \(x = \sum x_i b_i\). We denote \(\epsilon (b) := \prod _{i {\lt} j}(a_i, a_j)\).
If \(n=1\), then \(\epsilon (f) = 1\). If \(n=2\), then \(\epsilon (f) = 1\) if and only if the form \(Z^2 - a_1 X^2 - a_2 Y^2\) represents \(0\). By Corollary 3.1.13, this is equivalent to \(a_1 X^2 + a_2 Y^2\) representing \(1\), which means that there exists \(v \in V\) with \(Q(v) = 1\); this is independent on \(b\). For \(n \ge 3\) we use induction on \(n\). By Theorem 3.1.7, it suffices to prove that for any pair of contiguous bases \(b\) and \(b'\), we have \(\epsilon (b) = \epsilon (b')\). Thanks to the symmetry of the Hilbert symbol, \(\epsilon (b)\) is unchanged by permutation of the basis elements, so we may assume that \(b_1 = b_1'\). Then \(b_1' \cdot b_1' = a_1\), and we can write
Analogously,
The result follows by combining \(a_1 = a_1'\) and the induction hypothesis applied to the orthogonal complement of \(e_1\).
Let \(k\) be either \(\mathbb {Q}_p\) or \(\mathbb {R}\). Let \(f\) be a quadratic form of rank \(3\) over \(k\). Then \(f\) represents \(0\) if and only if \((-1, -d(f)) = \epsilon (f)\).
\(f\) is equivalent to \(aX^2 + bY^2 + cZ^2\) for some \(a, b, c \in k^\times \), and \(f\) represents \(0\) if and only if the form \(-caX^2 -cbY^2 - Z^2\) represents \(0\).
By the definition of Hilbert symbol, this last form represents \(0\) if and only if \((-ca, -cb) = 1\). This is equivalent to
By Proposition 2.1.4 (vi), \((c, c) = (-1, c)\), so this can be rewritten as
or equivalently, \((-1, -d(f)) = \epsilon (f)\).
Let \(k\) be either \(\mathbb {Q}_p\) or \(\mathbb {R}\). Let \(f\) be a quadratic form of rank \(2\) over \(k\), and let \(a \in k^\times / {k^\times }^2\). Then \(f\) represents \(a\) if and only if \((a, -d(f)) = \epsilon (f)\).
Up to equivalence, we may assume \(f = X^2 + bY^2\) for some \(b \in k^\times \). By Corollary 3.1.14, \(f\) represents \(a\) if and only if \(f_a := f \dotminus aZ^2\) represents \(0\), which by Lemma 3.2.4 is equivalent to \((-1, -d(f_a)) = \epsilon (f_a)\).
A computation shows that \(d(f_a) = -a d(f)\) and \(\epsilon (f_a) = (a, -d(f)) \epsilon (f)\). Combining this with Proposition 2.1.4, we conclude the result.
3.3 Hasse–Minkowski
The goal of this section is to prove the Hasse–Minkowski theorem over the rational numbers. To simplify the formalization process, rather than including a single long proof of this theorem, we will split it into smaller lemmas that can be formalized independently.
Denote by \(V\) the union of the set of prime numbers and the symbol \(\infty \), and denote \(\mathbb {Q}_\infty = \mathbb {R}\).
Let \(f\) be a quadratic form over \(\mathbb {Q}\). For each \(v \in V\), the injection \(\mathbb {Q}\to \mathbb {Q}_v\) allows one to view \(f\) as a quadratic form over \(\mathbb {Q}_v\), which we will denote \(f_v\).
A quadratic form \(f\) with coefficients in \(\mathbb {Q}\) is everywhere locally isotropic if \(f_v\) is isotropic for all \(v \in V\).
Let \(f\) be a quadratic form over \(\mathbb {Q}\). Then \(f\) is isotropic if and only if \(f\) is everywhere locally isotropic. In other words, \(f\) has a global zero if and only if \(f\) has everywhere a local zero.
Follows from the results below.
Let \(f\) be a degenerate quadratic form over \(\mathbb {Q}\). Then \(f\) is isotropic if and only if \(f\) is everywhere locally isotropic. In other words, \(f\) has a global zero if and only if \(f\) has everywhere a local zero.
Follows from the fact that every anisotropic quadratic form is nondegenerate.
From now on, given 3.3.3, we may assume that \(f\) is a nondegenerate quadratic form.
Let \(f\) be an isotropic quadratic form over \(\mathbb {Q}\). Then \(f\) is everywhere locally isotropic.
Any nontrivial solution over \(Q\) yields a solution over \(Q_v\) for any \(v \in V\).
Let \(f\) be a quadratic form over \(\mathbb {Q}\) of rank zero which is everywhere locally isotropic. Then \(f\) is isotropic.
Suffices to see that every rank zero quadratic form over a field is anisotropic.
Let \(K\) be a field of characteristic not equal to \(2\), let \(M\) be a \(K\)-vector space of positive dimension \(n\) and let \(f : M \to K\) be a nondegenerate quadratic form. Then there exists a form \(X_1^2 + a_2X_2^2 + \cdots + a_nX_n^2\) for some \(a_i \in K^\times \) such that it is isotropic if and only if \(f\) is.
Note that Mathlibcontains a similar statement 1 , where the coefficient of \(X_1\) is not assumed to be \(1\).
Let \(K\) be a field of characteristic not equal to \(2\), let \(M\) be a \(K\)-vector space of positive dimension \(n\) and let \(f : M \to K\) be a nondegenerate quadratic form. Then there exists a form \(X_1^2 + a_2X_2^2 + \cdots + a_nX_n^2\), for some squarefree \(a_i \in K^\times \) such that it is isotropic if and only if \(f\) is.
Follows from Lemma 3.3.6.
Let \(f\) be a quadratic form over \(\mathbb {Q}\) of rank one which is everywhere locally isotropic. Then \(f\) is isotropic.
Suffices to see that every nonzero quadratic form of rank one over a field is anisotropic.
Let \(f\) be a quadratic form over \(\mathbb {Q}\) of rank two which is everywhere locally isotropic. Then \(f\) is isotropic.
\(f\) is equivalent to \(X_1^2 - aX_2^2\), for some nonzero \(a\), which is positive because \(f_\infty \) represents \(0\). Write
Since \(f_p\) represents \(0\), \(a\) is a square in \(\mathbb {Q}_p\), so \(v_p(a)\) is even. It follows that \(a\) is a square in \(\mathbb {Q}\) and \(f\) represents \(0\).
Let \(f\) be a quadratic form over \(\mathbb {Q}\) of rank three which is everywhere locally isotropic. Then \(f\) is isotropic.
\(f\) is equivalent to \(X_1^2 - a X_2^2 - b X_3^2\); since we can multiply \(a\) and \(b\) by squares, we can reduce to the case where \(a\) and \(b\) are square-free integers. We can also assume \(|a| \le |b|\). We use induction on \(m := |a| + |b|\).
If \(m = 2\), then \(f \sim X_1^2 \pm X_2^2 \pm X_3^2\). The case \(X_1^2 + X_2^2 + X_3^2\) is excluded by the hypothesis that \(f_\infty \) represents zero. In the other cases, \(f\) represents zero (take e.g. \((1, 1, 0)\) or \((1, 0, 1)\), respectively).
Suppose now that \(m {\gt} 2\), that is, \(|b| \ge 2\) and write \(b = \pm p_1 \cdots p_k\), where the \(p_i\) are distinct primes. Let \(p\) be one of the \(p_i\); we will show that \(a\) is a square modulo \(p\). This is obvious if \(a \equiv 0 \mod p\). Otherwise \(a\) is a \(p\)-adic unit, and by hypothesis there exists \((x, y, z) \in \mathbb {Q}_p^3\) such that \(z^2 - ax^2 - by^2 = 0\). By Proposition 1.1.2, we can suppose that \((x, y, z)\) is primitive. From \(z^2 - a x^2 \equiv 0 \mod p\), we deduce that if \(x \equiv 0 \mod p\), then \(z \equiv 0 \mod p\) and \(p^2\) divides \(by^2\); since \(v_p(b) = 1\), this implies \(y \equiv 0 \mod p\), contradicting the assumption that \((x, y, z)\) is primitive. Therefore \(x \not\equiv 0 \mod p\) and \(a\) is a square modulo \(p\).
Since \(\mathbb {Z}/ b\mathbb {Z}= \prod _i \mathbb {Z}/ p_i \mathbb {Z}\), we also have that \(a\) is a square modulo \(b\), so there exist integers \(t, b'\) such that \(bb' = t^2 - a\) and we can choose \(t\) so that \(|t| \le |b|/2\). Then \(bb'\) is a norm of the extension \(k(\sqrt{a})/k\) for \(k = \mathbb {Q}\), \(\mathbb {R}\) or \(\mathbb {Q}_p\). From this we conclude that \(f\) represents \(0\) in \(k\) if and only if the same is true for \(f' := X_1^2 - a X_2^2 - b' X_3^2\) (see the proof of [ ).
In particular, \(f'\) represents \(0\) in each \(\mathbb {Q}_v\). But we have
Write \(b' = b'' u^2\), with \(b'', u\) integers and \(b''\) square-free, so \(|b''| {\lt} |b|\). We can then apply the induction hypothesis to the form \(X_1^2 - a X_2^2 - b'' X_3^2\), which is equivalent to \(f'\); hence \(f'\) represents \(0\) in \(\mathbb {Q}\) and so does \(f\).
Let \(f\) be a quadratic form over \(\mathbb {Q}\) of rank four which is everywhere locally isotropic. Then \(f\) is isotropic.
Up to equivalence, we may assume \(f = aX_1^2 + bX_2^2 - (cX_3^2 + dX_4^2)\). Fix a place \(v \in V\). Since \(f_v\) represents \(0\), Corollary 3.1.14 shows that there exists \(x_v \in \mathbb {Q}_v^\times \) which is represented both by \(aX_1^2 + bX_2^2\) and by \(cX_3^2 + dX_4^2\).
By Lemma 3.2.5, this is equivalent to saying that
Since \(\displaystyle \prod _{v \in V} (a, b)_v = \prod _{v \in V} (c, d)_v = 1\) by Theorem 2.1.13, we can deduce from Theorem 2.1.16 the existence of \(x \in \mathbb {Q}^\times \) such that
This shows that the form \(aX_1^2 + bX_2^2 - xZ^2\) represents zero in each \(\mathbb {Q}_v\), so by Lemma 3.3.10, it also represents \(0\) in \(\mathbb {Q}\). By Corollary 3.1.13, \(x\) is represented by \(aX_1^2 + bX_2^2\). The same argument shows that \(x\) is represented by \(cX_1^2 + dX_2^2\). By applying Corollary 3.1.14 again, we conclude that \(f\) represents \(0\).
Let \(f\) be a quadratic form over \(\mathbb {Q}\) of rank \(n \ge 5\) which is everywhere locally isotropic. Then \(f\) is isotropic.
The proof uses induction on \(n\). Write \(f = h - g\), where \(h = a_1X_1^2 + a_2X_2^2\), \(g = -(a_3X_3^2 + \cdots + a_nX_n^2)\). Let \(S\) be the finite subset of \(V\) consisting of \(\infty , 2\), and the primes \(p\) such that \(v_p(a_i) \ne 0\) for \(i \ge 3\). Let \(v \in S\). Since \(f_v\) represents \(0\), there exists \(c_v \in \mathbb {Q}_v^\times \) which is represented in \(\mathbb {Q}_v\) by \(h\) and \(g\), that is, there exist \(x_i^v \in \mathbb {Q}_v\), \(i=1, \dots , n\) (with \(x_i^v \ne 0\) for \(i=1, 2\), and some \(i \ge 3\)) such that
By Theorem 1.2.1, the squares of \(\mathbb {Q}_p^\times \) form an open set. Combining this with the approximation theorem 2.1.15, we deduce the existence of \(x_1, x_2 \in \mathbb {Q}^\times \) such that, denoting \(c := h(x_1, x_2)\), one has \(c/c_v \in {\mathbb {Q}_v^\times }^2\) for all \(v \in S\).
Consider the form \(f_1 := cZ^2 - g\). For each \(v \in S\), \(g\) represents \(c_v\) in \(\mathbb {Q}_v\), and hence also \(c\) because \(c/c_v \in {\mathbb {Q}_v^\times }^2\), hence \(f_1\) represents \(0\) in \(\mathbb {Q}_v\) by Corollary 3.1.13. For \(v \notin S\), the coefficients \(-a_3, \dots , -a_n\) of \(g\) are \(v\)-adic units, so the discriminant \(d_v(g)\) is a \(v\)-adic unit and \(\epsilon _v(g)=1\).
In all cases, \(f_q\) represents \(0\) in all \(\mathbb {Q}_v\), and since the rank of \(f\) is \(n-1\), the inductive hypothesis shows that \(f_1\) represents \(0\) in \(\mathbb {Q}\), or equivalently by Corollary 3.1.13, \(g\) represents \(c\) in \(\mathbb {Q}\). But \(h\) also represents \(c\), so by Corollary 3.1.14 \(f\) represents \(0\).