Hilbert symbols of binary forms

Isometric regular binary diagonal forms have the same norm-equation Hilbert symbol. This is the binary-step input for descending the pairwise product of Hilbert symbols along a diagonal chain, and hence for defining the local Hasse invariant on isometry classes. That assertion holds over any field in which two is invertible.

Over an arbitrary field, the norm-equation symbol also describes the scalar multiples of the binary form ⟨1, -b⟩, the norm form of the quadratic algebra K[√b] = QuadraticAlgebra K b 0 (the field K(√b) only when b is not a square): the multiple ⟨a, -ab⟩ is isometric to it exactly when (b, a) = 1, that is, when a is a value of ⟨1, -b⟩. Since the two planes always have the same dimension and discriminant, this makes the substitution of ⟨a, -ab⟩ for ⟨1, -b⟩ a controlled change of isometry class: read over the completions of a global field, it changes the local class exactly at the places where the symbol (b, a) is -1.

Main results

• TauCeti.hilbertSymbol_eq_of_equivalent_binary: isometric binary diagonal forms have the same Hilbert symbol.
• TauCeti.equivalent_binary_one_neg_iff_hilbertSymbol_eq_one: ⟨1, -b⟩ ≅ ⟨a, -ab⟩ exactly when (b, a) = 1.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter V, Proposition 3.18.
• J.-P. Serre, A Course in Arithmetic, Chapter IV, §2.1.
• O. T. O'Meara, Introduction to Quadratic Forms, 72:1, for the substitution of ⟨a, -ab⟩ for ⟨1, -b⟩.

theorem TauCeti.hilbertSymbol_eq_of_equivalent_binary {K : Type u_1} [Field K] [Invertible 2] {a b c d : Kˣ} (h : (QuadraticMap.weightedSumSquares K ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares K ![↑c, ↑d])) : hilbertSymbol a b = hilbertSymbol c d

Isometric regular binary diagonal forms have the same norm-equation Hilbert symbol.

theorem TauCeti.equivalent_binary_one_neg_iff_hilbertSymbol_eq_one {K : Type u_1} [Field K] (a b : Kˣ) : (QuadraticMap.weightedSumSquares K ![1, -↑b]).Equivalent (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) ↔ hilbertSymbol b a = 1

Scaling the norm form. The binary forms ⟨1, -b⟩ and ⟨a, -ab⟩ = a⟨1, -b⟩ are isometric exactly when the Hilbert symbol (b, a) is 1, that is, when a is a value of ⟨1, -b⟩. The two forms always have the same discriminant -b modulo squares.