Isotropy of quadratic forms over a local field, rank by rank

Let K be a nonarchimedean local field in which 2 is invertible. Whether a regular quadratic form over K is isotropic is decided by its rank n, its plain discriminant d ∈ Kˣ/(Kˣ)² and its local Hasse invariant s = ∏_{i<j} (aᵢ, aⱼ)_K:

• n = 1: never isotropic, and n = 2: isotropic exactly when d = [-1]; these two hold over every field (TauCeti.RegularFormClass.anisotropic_of_rank_le_one, TauCeti.RegularFormClass.not_anisotropic_iff_discr_eq_neg_one_of_rank_eq_two);
• n = 3: isotropic exactly when s = (-1, -d)_K;
• n = 4: isotropic exactly when d ≠ [1], or d = [1] and s = (-1, -1)_K;
• n ≥ 5: always isotropic.

In particular the u-invariant of K is four: every regular form of rank at least five is isotropic, and there is an anisotropic form of rank four, namely any form with invariants (4, [1], -(-1, -1)_K).

The ternary and quaternary criteria reduce to the binary one, which says that a regular binary form ⟨a, b⟩ represents a unit c exactly when (c, -ab)_K = (a, b)_K. A ternary form ⟨a, b, c⟩ is isotropic exactly when ⟨a, b⟩ represents -c. A quaternary form ⟨a, b⟩ ⊥ ⟨c, d⟩ is isotropic exactly when ⟨a, b⟩ and ⟨-c, -d⟩ have a common nonzero value, which is a question about the two characters (·, -ab)_K and (·, -cd)_K of Kˣ: they are distinct when abcd is a nonsquare, and two distinct nontrivial characters of a group of exponent two take every pair of values. A form of rank five contains a binary form, whose values fill two square classes, and a ternary form, which represents every unit outside one square class.

Main results

• TauCeti.RegularFormClass.not_anisotropic_iff_localHasse_eq_of_rank_eq_three: the ternary criterion s = (-1, -d)_K.
• TauCeti.RegularFormClass.not_anisotropic_iff_discr_ne_zero_or_localHasse_eq_of_rank_eq_four: the quaternary criterion d ≠ [1] ∨ s = (-1, -1)_K.
• TauCeti.RegularFormClass.not_anisotropic_of_five_le_rank: every class of rank at least five is isotropic.
• TauCeti.RegularFormClass.exists_rank_eq_four_and_anisotropic: there is an anisotropic class of rank four, so u(K) = 4.
• TauCeti.neg_mem_unitValueSet_presentedForm_three_of_not_isSquare: a ternary diagonal form represents every unit outside one square class.
• QuadraticForm.not_anisotropic_iff_localHasse_eq_of_finrank_eq_three, QuadraticForm.not_anisotropic_iff_discr_ne_zero_or_localHasse_eq_of_finrank_eq_four, QuadraticForm.not_anisotropic_of_five_le_finrank: the same criteria for regular forms on finite-dimensional spaces.
• QuadraticForm.exists_mem_unitValueSet_and_mem_of_five_le_finrank_add: two regular spaces of positive dimension whose dimensions sum to at least five represent a common nonzero value.
• QuadraticForm.exists_nondegenerate_and_anisotropic_fin_four: an anisotropic regular form on Fin 4 → K.

References

• J.-P. Serre, A Course in Arithmetic, Chapter IV, §2.2, Theorem 6.
• O. T. O'Meara, Introduction to Quadratic Forms, §63:17–63:19.
• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter VI, §2.

Diagonal forms of rank three, four and five

theorem TauCeti.not_anisotropic_presentedForm_three_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (w : Fin 3 → Kˣ) : ¬QuadraticMap.Anisotropic (presentedForm ⟨3, w⟩) ↔ hilbertSymbol (w 0) (w 1) * hilbertSymbol (w 0) (w 2) * hilbertSymbol (w 1) (w 2) = hilbertSymbol (-1) (-(w 0 * w 1 * w 2))

Ternary isotropy (Serre IV Thm 6 (ii)). A diagonal form ⟨a, b, c⟩ over K is isotropic exactly when its local Hasse invariant (a, b)(a, c)(b, c) is (-1, -abc)_K.

theorem TauCeti.not_anisotropic_presentedForm_four_of_not_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (w : Fin 4 → Kˣ) (h : ¬IsSquare (w 0 * w 1 * w 2 * w 3)) : ¬QuadraticMap.Anisotropic (presentedForm ⟨4, w⟩)

Quaternary isotropy, nonsquare discriminant (Serre IV Thm 6 (iii)). A diagonal form ⟨a, b, c, d⟩ over K whose discriminant abcd is a nonsquare is isotropic.

theorem TauCeti.not_anisotropic_presentedForm_four_iff_of_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (w : Fin 4 → Kˣ) (h : IsSquare (w 0 * w 1 * w 2 * w 3)) : ¬QuadraticMap.Anisotropic (presentedForm ⟨4, w⟩) ↔ hilbertSymbol (w 0) (w 1) * hilbertSymbol (w 0) (w 2) * hilbertSymbol (w 0) (w 3) * hilbertSymbol (w 1) (w 2) * hilbertSymbol (w 1) (w 3) * hilbertSymbol (w 2) (w 3) = hilbertSymbol (-1) (-1)

Quaternary isotropy, square discriminant (Serre IV Thm 6 (iii)). A diagonal form ⟨a, b, c, d⟩ over K whose discriminant abcd is a square is isotropic exactly when its local Hasse invariant ∏_{i<j} (aᵢ, aⱼ)_K is (-1, -1)_K.

theorem TauCeti.neg_mem_unitValueSet_presentedForm_three_of_not_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (w : Fin 3 → Kˣ) (x : Kˣ) (hx : ¬IsSquare (x * (w 0 * w 1 * w 2))) : -x ∈ QuadraticMap.unitValueSet (presentedForm ⟨3, w⟩)

Ternary representation. A diagonal form ⟨a, b, c⟩ over K represents -x for every unit x such that xabc is a nonsquare: a ternary form represents every unit outside one square class.

theorem TauCeti.not_anisotropic_presentedForm_five {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (w : Fin 5 → Kˣ) : ¬QuadraticMap.Anisotropic (presentedForm ⟨5, w⟩)

Isotropy in rank five (Serre IV Thm 6 (iv)). Every diagonal form of rank five over K is isotropic.

theorem TauCeti.not_anisotropic_presentedForm_of_five_le {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {n : ℕ} (hn : 5 ≤ n) (w : Fin n → Kˣ) : ¬QuadraticMap.Anisotropic (presentedForm ⟨n, w⟩)

Isotropy in rank at least five. Every diagonal form of rank at least five over K is isotropic.

The isotropy list on isometry classes

theorem TauCeti.RegularFormClass.not_anisotropic_iff_localHasse_eq_of_rank_eq_three {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x : RegularFormClass K} (hx : x.rank = 3) : ¬x.Anisotropic ↔ x.localHasse = hilbertSymbolOnSquareClasses (squareClass (-1)) (squareClass (-1) + x.discr)

Ternary isotropy (Serre IV Thm 6 (ii)). A regular-form class of rank three over K is isotropic exactly when its local Hasse invariant is (-1, -d)_K, where d is its discriminant.

theorem TauCeti.RegularFormClass.not_anisotropic_iff_discr_ne_zero_or_localHasse_eq_of_rank_eq_four {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x : RegularFormClass K} (hx : x.rank = 4) : ¬x.Anisotropic ↔ x.discr ≠ 0 ∨ x.localHasse = hilbertSymbol (-1) (-1)

Quaternary isotropy (Serre IV Thm 6 (iii)). A regular-form class of rank four over K is isotropic exactly when its discriminant is not the class of 1, or its discriminant is the class of 1 and its local Hasse invariant is (-1, -1)_K.

theorem TauCeti.RegularFormClass.not_anisotropic_of_five_le_rank {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x : RegularFormClass K} (hx : 5 ≤ x.rank) : ¬x.Anisotropic

Isotropy in rank at least five (Serre IV Thm 6 (iv)). Every regular-form class of rank at least five over K is isotropic.

theorem TauCeti.RegularFormClass.exists_rank_eq_four_and_anisotropic {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : ∃ (x : RegularFormClass K), x.rank = 4 ∧ x.Anisotropic

u(K) = 4 (O'Meara 63:19). There is an anisotropic regular-form class of rank four over K: any class with trivial discriminant and local Hasse invariant -(-1, -1)_K.

The isotropy list on quadratic forms

theorem QuadraticForm.not_anisotropic_iff_localHasse_eq_of_finrank_eq_three {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 3) : ¬QuadraticMap.Anisotropic Q ↔ (TauCeti.formClass Q hQ).localHasse = TauCeti.hilbertSymbolOnSquareClasses (TauCeti.squareClass (-1)) (TauCeti.squareClass (-1) + (TauCeti.formClass Q hQ).discr)

Ternary isotropy (Serre IV Thm 6 (ii)). A regular quadratic form on a space of dimension three over K is isotropic exactly when its local Hasse invariant is (-1, -d)_K, where d is its discriminant.

theorem QuadraticForm.not_anisotropic_iff_discr_ne_zero_or_localHasse_eq_of_finrank_eq_four {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 4) : ¬QuadraticMap.Anisotropic Q ↔ (TauCeti.formClass Q hQ).discr ≠ 0 ∨ (TauCeti.formClass Q hQ).localHasse = TauCeti.hilbertSymbol (-1) (-1)

Quaternary isotropy (Serre IV Thm 6 (iii)). A regular quadratic form on a space of dimension four over K is isotropic exactly when its discriminant is not the class of 1, or its discriminant is the class of 1 and its local Hasse invariant is (-1, -1)_K.

theorem QuadraticForm.not_anisotropic_of_five_le_finrank {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : 5 ≤ Module.finrank K V) : ¬QuadraticMap.Anisotropic Q

Isotropy in dimension at least five (Serre IV Thm 6 (iv)). Every regular quadratic form on a space of dimension at least five over K is isotropic.

theorem QuadraticForm.exists_mem_unitValueSet_and_mem_of_five_le_finrank_add {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (R : QuadraticForm K W) (hR : QuadraticMap.Nondegenerate) (hV : 0 < Module.finrank K V) (hW : 0 < Module.finrank K W) (hVW : 5 ≤ Module.finrank K V + Module.finrank K W) : ∃ a ∈ QuadraticMap.unitValueSet Q, a ∈ QuadraticMap.unitValueSet R

Two regular local quadratic spaces of positive dimension whose dimensions sum to at least five represent a common nonzero value: their difference is isotropic by the bound in dimension at least five.

theorem QuadraticForm.exists_nondegenerate_and_anisotropic_fin_four {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : ∃ (Q : QuadraticForm K (Fin 4 → K)), QuadraticMap.Nondegenerate ∧ QuadraticMap.Anisotropic Q

u(K) = 4 (O'Meara 63:19). There is an anisotropic regular quadratic form on the four-dimensional space Fin 4 → K.