Binary forms with unit coefficients over a Henselian local ring

Let R be a Henselian local ring whose residue field is finite and in which 2 is a unit. Then every binary form a x² + b y² with unit coefficients represents every unit c of R.

Over the finite residue field of odd characteristic this is the universality of regular binary forms. Since c is a unit, one of the two coordinates of a residue solution is nonzero; the other coordinate is lifted arbitrarily, and the nonzero one is lifted by Hensel's lemma, which applies because the derivative 2x of X² - u is a unit there.

A consequence is that a diagonal quadratic form with at least three unit coefficients is isotropic: a x² + b y² = -c gives the nonzero isotropic vector (x, y, 1). Over the ring of integers of a nonarchimedean local field of odd residue characteristic, this makes a fixed regular form over a number field isotropic at almost every finite place.

Main results

• TauCeti.exists_mul_sq_add_mul_sq_eq_of_isUnit: a x² + b y² = c is solvable in R when a, b and c are units.

References

• J.-P. Serre, A Course in Arithmetic, Chapter I, §2 (quadratic forms over finite fields) and Chapter II, §2 (lifting solutions by Hensel's lemma).

theorem TauCeti.exists_mul_sq_add_mul_sq_eq_of_isUnit {R : Type u_1} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] (h2 : IsUnit 2) {a b c : R} (ha : IsUnit a) (hb : IsUnit b) (hc : IsUnit c) : ∃ (x : R) (y : R), a * x ^ 2 + b * y ^ 2 = c

Binary forms with unit coefficients are universal over a Henselian local ring. If the residue field of the Henselian local ring R is finite and 2 is a unit of R, then for units a, b and c there are x and y with a x² + b y² = c.