The archimedean Hasse sign of a quadratic form over a number field

For a diagonalization of a quadratic form over a number field by global units, this file computes the product of the real Hilbert symbols of the localized coefficients over the ordered pairs of indices: it is (-1)^(q(q-1)/2), where q is the negative index of the form at the real place. In particular the product depends on the form and the place alone, not on the chosen diagonalization; it is the archimedean factor of the product over all places of the Hasse signs of a global form.

The archimedean classification that supplies the negative index is TauCeti.NumberTheory.QuadraticForm.Global.Signature at the real places and TauCeti.NumberTheory.QuadraticForm.Global.ComplexPlaces through the complex embeddings.

Main results

• TauCeti.prod_hilbertSymbol_unitAtRealPlace_of_equiv_weightedSumSquares: the archimedean Hasse sign of a diagonalization.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 71:18 for the real Hilbert symbol and §61 for the archimedean classification.

theorem TauCeti.prod_hilbertSymbol_unitAtRealPlace_of_equiv_weightedSumSquares {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {ι : Type u_3} [Fintype ι] [LinearOrder ι] {Q : QuadraticForm K V} {a : ι → Kˣ} (h : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K fun (i : ι) => ↑(a i))) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : ∏ ij : ι × ι with ij.1 < ij.2, hilbertSymbol ((unitAtRealPlace w) (a ij.1)) ((unitAtRealPlace w) (a ij.2)) = (-1) ^ (Q.realNegativeIndex w).choose 2

The archimedean Hasse sign. For a diagonalization Q ≃ ⟨a₁, …, aₙ⟩ by global units, the product of the real Hilbert symbols of the localized coefficients over the ordered pairs i < j is (-1)^(q(q-1)/2), where q is the negative index of Q at the real place. In particular the product depends on Q and the place alone, not on the chosen diagonalization.