Binary quadratic forms over a local field

Over a nonarchimedean local field of characteristic different from two, a binary regular quadratic form is determined by its discriminant and local Hasse invariant. Its nonzero represented values are determined by the same invariants: ⟨a, b⟩ represents a unit c exactly when (c, -ab) = (a, b). This describes both the hyperbolic case, which represents every unit, and the anisotropic case, whose values form a coset of the quadratic norm group.

The representation criterion is stated for arbitrary regular binary spaces, so a caller need not choose a diagonalization. These are the binary inputs to classification by splitting off a represented line and cancelling.

References

• J.-P. Serre, A Course in Arithmetic, Chapter IV, §2.2, Theorem 6 and its corollary, and §2.3, Theorem 7, in dimension two.
• O. T. O'Meara, Introduction to Quadratic Forms, §63:20–21.

theorem TauCeti.mem_unitValueSet_binary_iff_hilbertSymbol_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (a b c : Kˣ) : c ∈ (QuadraticMap.weightedSumSquares K ![↑a, ↑b]).unitValueSet ↔ hilbertSymbol c (-(a * b)) = hilbertSymbol a b

A binary diagonal form over a local field represents a unit c exactly when its Hilbert symbol with the negative discriminant equals the local Hasse invariant of the form.

theorem TauCeti.equivalent_binary_iff_isSquare_and_hilbertSymbol_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (a b c d : Kˣ) : (QuadraticMap.weightedSumSquares K ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares K ![↑c, ↑d]) ↔ IsSquare (a * b * (c * d)) ∧ hilbertSymbol a b = hilbertSymbol c d

Local binary classification. Two binary diagonal forms over a nonarchimedean local field are isometric exactly when their discriminants and local Hasse invariants agree.

theorem QuadraticForm.mem_unitValueSet_iff_hilbertSymbol_eq_localHasse_of_finrank_eq_two {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 = 2) (c : Kˣ) : c ∈ QuadraticMap.unitValueSet Q ↔ TauCeti.hilbertSymbolOnSquareClasses (TauCeti.squareClass c) (TauCeti.squareClass (-1) + (TauCeti.formClass Q hQ).discr) = (TauCeti.formClass Q hQ).localHasse

The represented units of a regular binary space. A unit c is represented exactly when its Hilbert symbol with the negative discriminant equals the local Hasse invariant of the space. The discriminant is the plain discriminant, written in the additive square-class group.