A quadratic form $Q$ on a module $M$ is isotropic if it has a nontrivial zero, i.e., there exists $v \neq 0$ with $Q(v) = 0$.
Instances For
The diagonal quadratic form $\sum_i a_i x_i^2$ with rational coefficients $a_0, \dots, a_{n-1} \in \mathbb{Q}$.
Instances For
If a diagonal quadratic form is isotropic over $\mathbb{Q}$, then it remains isotropic over any $\mathbb{Q}$-algebra $F$ (by extending scalars).
A binary diagonal form $a_0 x_0^2 + a_1 x_1^2$ is isotropic over a $\mathbb{Q}$-algebra $F$ iff $a_0 = 0$, $a_1 = 0$, or $-a_0 a_1$ is a square in $F$.
A positive natural number with even $p$-adic valuation at every prime $p$ is a perfect square.
If a nonzero rational $q$ is a square in $\mathbb{Q}_p$, then its $p$-adic valuation is even.
If a rational $q = m/n$ (in lowest terms) has even $p$-adic valuation, then both $\mathrm{val}_p(m)$ and $\mathrm{val}_p(n)$ are even.
Local-global for squares. A rational number $q$ is a square in $\mathbb{Q}$ iff it is a square in $\mathbb{R}$ and a square in $\mathbb{Q}_p$ for every prime $p$.
Hasse-Minkowski for binary forms ($n = 2$). A binary diagonal form over $\mathbb{Q}$ is isotropic iff it is isotropic over $\mathbb{R}$ and over every $\mathbb{Q}_p$.
For a ternary diagonal form with all coefficients nonzero, isotropy over $F$ is equivalent
to the TernaryForm.RepresentsZero predicate on the corresponding units of $F$.
Specialization of diagQuadFormOver_isIsotropic_iff_ternary_represents_zero to
$F = \mathbb{Q}$.
Hasse-Minkowski representation principle for binary forms. If a binary form $u x^2 + v y^2$ represents $t \neq 0$ over $\mathbb{R}$ and over every $\mathbb{Q}_p$, then it represents $t$ over $\mathbb{Q}$.
Hasse-Minkowski for ternary forms (core step). A ternary form $u x^2 + v y^2 + w z^2$ with $u, v, w \in \mathbb{Q}^\times$ represents zero over $\mathbb{Q}$ provided it does so over $\mathbb{R}$ and over every $\mathbb{Q}_p$. The reduction uses the binary representation theorem applied to $u x^2 + v y^2 = -w$.
Bridge from the ternary Hasse-Minkowski core (stated in terms of units and
RepresentsZero) to isotropy of diagQuadForm.
Hasse-Minkowski for ternary forms ($n = 3$). A ternary diagonal form is isotropic over $\mathbb{Q}$ iff it is isotropic over $\mathbb{R}$ and over every $\mathbb{Q}_p$.
Real-side splitting: if a quaternary form $\sum_{i=0}^3 a_i x_i^2$ is isotropic over $\mathbb{R}$, then there is a sign $\sigma \in \{\pm 1\}$ such that $a_0 x^2 + a_1 y^2 - \sigma z^2$ and $a_2 x^2 + a_3 y^2 + \sigma z^2$ are both isotropic over $\mathbb{R}$.
$p$-adic splitting: if a quaternary form is isotropic over every $\mathbb{Q}_p$, there exists a rational $t \neq 0$ such that the two ternary forms $a_0 x^2 + a_1 y^2 - t z^2$ and $a_2 x^2 + a_3 y^2 + t z^2$ are both isotropic over every $\mathbb{Q}_p$.
Combining the real and $p$-adic splittings: for the rational $t$ from the $p$-adic splitting, the two ternary subforms are also isotropic over $\mathbb{R}$.
Splitting value for quaternary forms. Combining quaternary_split_padic_isotropy and
quaternary_split_real_isotropy: there exists a rational $t \neq 0$ such that both ternary
subforms $a_0 x^2 + a_1 y^2 - t z^2$ and $a_2 x^2 + a_3 y^2 + t z^2$ are isotropic over
$\mathbb{R}$ and over every $\mathbb{Q}_p$.
Assembly: from rational isotropy of two ternary subforms with the splitting value $t$, construct a rational isotropic vector for the original quaternary form.
Hasse-Minkowski for quaternary forms ($n = 4$). A quaternary diagonal form is isotropic over $\mathbb{Q}$ iff it is isotropic over $\mathbb{R}$ and over every $\mathbb{Q}_p$.
Given coefficients $a_0, \dots, a_{m+4}$ and a value $t$, form the "replaced" sequence $(t, a_2, a_3, \dots, a_{m+4})$ of length $m + 4$ (where the first two coefficients $a_0, a_1$ have been merged into a single value $t$).
Instances For
If the subform $\sum_{i \ge 2} a_i x_i^2$ is isotropic over $F$, then for any $t$, the replaced form is also isotropic over $F$ (set $x_0 = 0$).
Corollary 11.2 (cofinite local isotropy of subforms). For the subform with $m + 3 \ge 3$ variables, the form is isotropic over $\mathbb{Q}_p$ for all but finitely many primes $p$.
Scaling a coefficient $b_k$ by a nonzero square $u^2$ does not change whether the diagonal quadratic form is isotropic.
Specialization of diagQuadFormOver_isIsotropic_of_scale_coeff to scaling the first
coefficient.
The isotropy of a replaced form depends only on the square class of $t$ over $\mathbb{Q}$:
if $c = t \cdot u^2$ for some nonzero rational $u$, then replacedForm a c is isotropic iff
replacedForm a t is.
From isotropy of the full $(m+5)$-variable diagonal form $\sum a_i x_i^2$, either there is a nonzero rational splitting value $t$ such that the replaced $(m+4)$-variable form (with $a_0 x_0^2 + a_1 x_1^2$ replaced by $t \cdot y^2$) is isotropic over $F$, or the $(m+3)$-variable subform with coefficients $a_2, a_3, \dots, a_{m+4}$ is itself isotropic.
The $p$-adic isotropy of a replaced form depends only on the $p$-adic square class of $t$:
if $c$ and $t$ lie in the same square class over $\mathbb{Q}_p$, then replacedForm a c is
isotropic over $\mathbb{Q}_p$ iff replacedForm a t is.
The real isotropy of a replaced form depends only on the real square class of $t$ (i.e., on
$\mathrm{sign}(t)$): if $c$ and $t$ are positive multiples of one another in $\mathbb{R}$, then
replacedForm a c is isotropic over $\mathbb{R}$ iff replacedForm a t is.
If the full $(m+5)$-variable diagonal form is isotropic over $\mathbb{Q}_p$, then there
exists a nonzero rational splitting value $t$ such that the replaced $(m+4)$-variable form
replacedForm a t is isotropic over $\mathbb{Q}_p$.
If the full $(m+5)$-variable diagonal form is isotropic over $\mathbb{R}$, then there
exists a nonzero rational splitting value $t$ such that the replaced $(m+4)$-variable form
replacedForm a t is isotropic over $\mathbb{R}$.
Square-class weak approximation for binary forms. Given prescribed local splitting values $t_p$ for each $p \in S$ and a real splitting value $t_\mathbb{R}$, there exist rationals $x, y$ such that the value $a_0 x^2 + a_1 y^2$ is nonzero, lies in the same $p$-adic square class as $t_p$ for each $p \in S$, and lies in the same real square class as $t_\mathbb{R}$.
Given local isotropy of $\sum a_i x_i^2$ over $\mathbb{R}$ and every $\mathbb{Q}_p$, produce rationals $x, y$ such that $a_0 x^2 + a_1 y^2 \neq 0$ and the replaced $(m+4)$-variable form with this value is simultaneously isotropic over $\mathbb{R}$ and over $\mathbb{Q}_p$ for every $p \in S$. Combines local splitting values with the weak-approximation step.
Existence of a global splitting value for the large form: given everywhere-local isotropy of the $(m+5)$-variable diagonal form, there exist rationals $x, y$ with $a_0 x^2 + a_1 y^2 \neq 0$ such that the replaced $(m+4)$-variable form is isotropic over $\mathbb{R}$ and over every $\mathbb{Q}_p$. Combines the weak-approximation step (handling a finite "bad" set of primes) with a Chevalley-Warning-type result handling all remaining primes.
Assembly step. From an isotropic vector for the replaced $(m+4)$-variable form
replacedForm a (a 0 * x^2 + a 1 * y^2) over $\mathbb{Q}$, and rationals $x, y$ with the head
expression nonzero, construct an isotropic vector for the original $(m+5)$-variable form
diagQuadForm (m+5) a over $\mathbb{Q}$ by splitting the first coordinate into $(x v_0, y v_0)$.
Hasse-Minkowski inductive step ($n \geq 5$). Assuming the Hasse-Minkowski theorem holds for diagonal forms in $m + 4$ variables, deduce it for diagonal forms in $m + 5$ variables: find a splitting value, apply the induction hypothesis to the replaced form, and assemble the result.
Hasse-Minkowski (hard direction). If a diagonal quadratic form $\sum_{i < n} a_i x_i^2$ over $\mathbb{Q}$ is isotropic over $\mathbb{R}$ and over every $\mathbb{Q}_p$, then it is isotropic over $\mathbb{Q}$. Proof by induction on $n$: small cases ($n \leq 4$) and the inductive step for $n \geq 5$.
Theorem 9.10 (Hasse-Minkowski). A diagonal quadratic form $\sum_{i < n} a_i x_i^2$ over $\mathbb{Q}$ represents zero nontrivially if and only if it does so over $\mathbb{R}$ and over every $p$-adic field $\mathbb{Q}_p$.