The Hasse sign of a quadratic form at a finite place

For a regular quadratic form Q over a number field K and a finite place v of K, the finite Hasse sign Q.finiteHasse hQ v ∈ {±1} is the local Hasse invariant TauCeti.RegularFormClass.localHasse of the localization Q.atFinitePlace v over the completion K_v. If Q ≅ ⟨a₁, …, aₙ⟩ over K, it is the product ∏_{i<j} (aᵢ, aⱼ)_v of the Hilbert symbols of the localized coefficients, and it does not depend on the chosen diagonalization.

The discriminant square class of Q at v is the image of the global discriminant of Q in K_vˣ/(K_vˣ)², which is the discriminant of the localized form by QuadraticForm.discr_atFinitePlace. It is the only local datum besides the rank that enters the behaviour of the finite Hasse sign under the operations on forms:

• orthogonal sum: s_v(Q ⊥ R) = s_v(Q) · s_v(R) · (d_v(Q), d_v(R))_v;
• scaling by a ∈ Kˣ: s_v(a Q) = s_v(Q) · (a, -1)_v^{n(n-1)/2} · (a, d_v(Q))_v^{n-1};
• negation, the case a = -1;
• forms that are isometric at v, in particular globally isometric forms, have the same finite Hasse sign at v.

Together with the rank and the discriminant, the Hasse sign is one of the three invariants that classify regular quadratic forms over a nonarchimedean local field (O'Meara, §63).

Main definitions

• QuadraticForm.finiteHasse: the Hasse sign of a regular form at a finite place.

Main results

• QuadraticForm.finiteHasse_eq_localHasse_baseChange: the finite Hasse sign is the local Hasse invariant of the scalar extension of the global isometry class.
• QuadraticForm.finiteHasse_eq_prod_hilbertSymbol: its value ∏_{i<j} (aᵢ, aⱼ)_v on any diagonalization ⟨a₁, …, aₙ⟩ over K, and QuadraticForm.finiteHasse_weightedSumSquares_binary: the single symbol (a, b)_v for a binary form ⟨a, b⟩.
• QuadraticForm.finiteHasse_eq_of_equivalent_atFinitePlace, QuadraticMap.Equivalent.finiteHasse_eq: forms isometric at v, in particular isometric forms, have the same finite Hasse sign.
• QuadraticForm.finiteHasse_eq_one_of_finrank_le_one, QuadraticForm.finiteHasse_eq_one_of_finrank_eq_two: the finite Hasse sign is trivial in rank at most one, and in rank two wherever the discriminant is the class of -1.
• QuadraticForm.finiteHasse_prod, QuadraticForm.finiteHasse_smul, QuadraticForm.finiteHasse_neg: the orthogonal-sum, scaling and negation formulas.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter V, §3.
• J.-P. Serre, A Course in Arithmetic, Chapter IV, §2.1 and §3.1.
• O. T. O'Meara, Introduction to Quadratic Forms, §63.

noncomputable def QuadraticForm.finiteHasse {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ℤˣ

The Hasse sign of a regular quadratic form at a finite place v of a number field: the local Hasse invariant ∏_{i<j} (aᵢ, aⱼ)_v ∈ {±1} of the localization of Q at v, for any diagonalization ⟨a₁, …, aₙ⟩ of that localization over the completion K_v.

theorem QuadraticForm.finiteHasse_def {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Q.finiteHasse hQ v = (TauCeti.formClass (Q.atFinitePlace v) ⋯).localHasse

The finite Hasse sign is the local Hasse invariant of the class of the localized form.

theorem QuadraticForm.finiteHasse_eq_localHasse_baseChange {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Q.finiteHasse hQ v = (TauCeti.RegularFormClass.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TauCeti.formClass Q hQ)).localHasse

The finite Hasse sign is the local Hasse invariant of the scalar extension to K_v of the isometry class of Q over K.

theorem QuadraticForm.finiteHasse_eq_prod_hilbertSymbol {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {n : ℕ} {a : Fin n → Kˣ} (h : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(a i))) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Q.finiteHasse hQ v = ∏ i : Fin n, ∏ j > i, TauCeti.hilbertSymbol (v.unitAtFinitePlace (a i)) (v.unitAtFinitePlace (a j))

Independence of the diagonalization. If Q ≅ ⟨a₁, …, aₙ⟩ over K, the finite Hasse sign of Q at v is ∏_{i<j} (aᵢ, aⱼ)_v, the product of the Hilbert symbols over K_v of the images of the coefficients.

@[simp]

theorem QuadraticForm.finiteHasse_weightedSumSquares_binary {K : Type u} [Field K] [NumberField K] (a b : Kˣ) (h : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : finiteHasse (QuadraticMap.weightedSumSquares K ![↑a, ↑b]) h v = TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)

The finite Hasse sign of a binary diagonal form ⟨a, b⟩ at v is the single Hilbert symbol (a, b)_v of the images of its coefficients.

theorem QuadraticForm.finiteHasse_eq_of_equivalent_atFinitePlace {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (h : QuadraticMap.Equivalent (Q.atFinitePlace v) (R.atFinitePlace v)) : Q.finiteHasse hQ v = R.finiteHasse hR v

Isometry invariance. Regular forms whose localizations at v are isometric have the same finite Hasse sign at v.

theorem QuadraticMap.Equivalent.finiteHasse_eq {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (h : Equivalent Q R) (hQ : Nondegenerate) (hR : Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Q.finiteHasse hQ v = R.finiteHasse hR v

Isometric regular forms have the same finite Hasse sign at every finite place.

@[simp]

theorem QuadraticForm.finiteHasse_eq_one_of_finrank_le_one {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V ≤ 1) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Q.finiteHasse hQ v = 1

The finite Hasse sign of a form of rank at most one is trivial.

theorem QuadraticForm.finiteHasse_eq_one_of_finrank_eq_two {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 2) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hd : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass Q hQ).discr = TauCeti.squareClass (-1)) : Q.finiteHasse hQ v = 1

The finite Hasse sign of a binary form is trivial at every finite place v at which the image of its global discriminant in K_vˣ/(K_vˣ)² is the class of -1: there the localization is a hyperbolic plane.

theorem QuadraticForm.finiteHasse_prod {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (R : QuadraticForm K W) (hR : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : finiteHasse (QuadraticMap.prod Q R) ⋯ v = Q.finiteHasse hQ v * R.finiteHasse hR v * TauCeti.hilbertSymbolOnSquareClasses ((algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass Q hQ).discr) ((algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass R hR).discr)

The orthogonal-sum formula s_v(Q ⊥ R) = s_v(Q) · s_v(R) · (d_v(Q), d_v(R))_v, where d_v is the image in K_vˣ/(K_vˣ)² of the global discriminant.

theorem QuadraticForm.finiteHasse_smul {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (a : Kˣ) (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (↑a • Q).finiteHasse ⋯ v = Q.finiteHasse hQ v * TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (-1) ^ (Module.finrank K V).choose 2 * TauCeti.hilbertSymbolOnSquareClasses (TauCeti.squareClass (v.unitAtFinitePlace a)) ((algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass Q hQ).discr) ^ (Module.finrank K V - 1)

The scaling formula s_v(a Q) = s_v(Q) · (a, -1)_v^{n(n-1)/2} · (a, d_v(Q))_v^{n-1} for a ∈ Kˣ and a form Q of rank n, where d_v(Q) is the image in K_vˣ/(K_vˣ)² of the global discriminant.

theorem QuadraticForm.finiteHasse_neg {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (-Q).finiteHasse ⋯ v = Q.finiteHasse hQ v * TauCeti.hilbertSymbol (-1) (-1) ^ (Module.finrank K V).choose 2 * TauCeti.hilbertSymbolOnSquareClasses (TauCeti.squareClass (-1)) ((algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass Q hQ).discr) ^ (Module.finrank K V - 1)

The negation formula s_v(-Q) = s_v(Q) · (-1, -1)_v^{n(n-1)/2} · (-1, d_v(Q))_v^{n-1} for a form Q of rank n, where d_v(Q) is the image in K_vˣ/(K_vˣ)² of the global discriminant.