Quaternary descent

Let F be a field of characteristic not two and Q a regular quadratic form of dimension four over F whose discriminant is the square class of a nonsquare d. Let E = F(√d), a quadratic field extension of F. Then Q is isotropic over F exactly when its scalar extension to E is isotropic (O'Meara 58:7).

This is what makes a quaternary form accessible to arguments over the discriminant field: over E the discriminant of Q becomes a square, and the theorem descends isotropy back to F.

The hypotheses have the following roles.

• The dimension is exactly four. Over F = ℚ(i), the binary form ⟨1, 2⟩ has discriminant [2] and is anisotropic, as -2 is not a square in ℚ(i), but it becomes isotropic over F(√2), where -2 = (i√2)².
• The discriminant is the plain discriminant TauCeti.RegularFormClass.discr; in dimension four the signed discriminant differs from it by the class of -1.
• E is a quadratic extension of F containing a square root s of the nonsquare d, which pins it down as F(s). A larger field containing a square root of d, such as F(√d, √e), is not covered.

Main results

• QuadraticForm.not_anisotropic_of_not_anisotropic_baseChange_quaternary: quaternary descent of isotropy from F(√d) to F.
• QuadraticForm.anisotropic_baseChange_iff_quaternary: a quaternary form of nonsquare discriminant d is anisotropic over F(√d) exactly when it is anisotropic over F.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), 58:7.

theorem QuadraticForm.not_anisotropic_of_not_anisotropic_baseChange_quaternary {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [Invertible 2] [FiniteDimensional F V] {E : Type w} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] (Q : QuadraticForm F V) (hQ : QuadraticMap.Nondegenerate) (hdim : Module.finrank F V = 4) (d : Fˣ) (hd : (TauCeti.formClass Q hQ).discr = TauCeti.squareClass d) (hdsq : ¬IsSquare d) (s : E) (hs : s * s = (algebraMap F E) ↑d) (h : ¬QuadraticMap.Anisotropic (QuadraticForm.baseChange E Q)) : ¬QuadraticMap.Anisotropic Q

Quaternary descent (O'Meara 58:7). Let Q be a regular quadratic form of dimension four over a field F of characteristic not two, whose discriminant is the square class of a nonsquare d, and let E be a field of degree two over F containing a square root s of d, so that E = F(s). If Q is isotropic over E, then it is isotropic over F.

theorem QuadraticForm.anisotropic_baseChange_iff_quaternary {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [Invertible 2] [FiniteDimensional F V] {E : Type w} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] (Q : QuadraticForm F V) (hQ : QuadraticMap.Nondegenerate) (hdim : Module.finrank F V = 4) (d : Fˣ) (hd : (TauCeti.formClass Q hQ).discr = TauCeti.squareClass d) (hdsq : ¬IsSquare d) (s : E) (hs : s * s = (algebraMap F E) ↑d) : QuadraticMap.Anisotropic (QuadraticForm.baseChange E Q) ↔ QuadraticMap.Anisotropic Q

Quaternary descent, as an equivalence: a regular quaternary form whose discriminant is the square class of a nonsquare d is anisotropic over F(√d) exactly when it is anisotropic over F.