Quadratic forms over finite fields are isotropic in three or more variables

Over a finite field every quadratic form in at least three variables has a nonzero null vector. This is the Chevalley–Warning theorem applied to the polynomial GPR 11.8 attaches to the form: its total degree is 2, which is smaller than the number of variables, so the number of solutions of q = 0 is divisible by the characteristic. The zero vector is one solution, hence there are at least p ≥ 2 of them.

Over a field the two isotropy notions of the literature agree (QuadraticMap.isGPRIsotropic_iff_not_anisotropic), so this also produces a unimodular null vector in the sense of GPR 11.17.

Main results

• QuadraticForm.not_anisotropic_of_two_lt_finrank : over a finite field, a quadratic form on a space of dimension greater than two is not anisotropic.
• QuadraticForm.exists_ne_zero_apply_eq_zero_of_two_lt_finrank : the same, stated as the existence of a nonzero null vector.

Implementation notes

The count is run on the solution subtype {x : Fin n → K // eval x f = 0} that char_dvd_card_solutions speaks about. Rather than exhibiting two solutions directly, the proof assumes anisotropy, deduces that the subtype is a singleton, and concludes p ∣ 1; this avoids having to produce a second solution by hand.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.8, 23.14.
• [EKM] Elman, Karpenko, Merkurjev, The Algebraic and Geometric Theory of Quadratic Forms.

theorem QuadraticForm.not_anisotropic_of_two_lt_finrank {K : Type u} [Field K] [Finite K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (q : QuadraticForm K V) (h : 2 < Module.finrank K V) : ¬QuadraticMap.Anisotropic q

Chevalley–Warning for quadratic forms. Over a finite field, a quadratic form on a vector space of dimension greater than two is not anisotropic.

The polynomial GPR 11.8 attaches to q in a basis has total degree at most two, which is less than the number of variables, so the characteristic divides the number of its zeros. Anisotropy would make the zero vector the only one.

theorem QuadraticForm.exists_ne_zero_apply_eq_zero_of_two_lt_finrank {K : Type u} [Field K] [Finite K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (q : QuadraticForm K V) (h : 2 < Module.finrank K V) : ∃ (v : V), v ≠ 0 ∧ q v = 0

Chevalley–Warning for quadratic forms, stated as the existence of a nonzero null vector.