The system of local invariants of a global quadratic form

A regular quadratic form Q of rank n over a number field K determines a system of local invariants Q.globalInvariants hQ : GlobalFormInvariants K: its rank n, its plain discriminant d(Q) ∈ Kˣ/(Kˣ)², its Hasse sign s_v(Q) at every finite place v, and its positive index p_w(Q) at every real place w. Isometric forms have the same system.

Apart from the positivity of the rank and the product relation, every condition of GlobalFormInvariants.IsAdmissible holds for such a system:

• at a real place p_w ≤ n, and the image of d(Q) is (-1)^(n - p_w), by the determinant-sign formula;
• the finite Hasse signs are trivial at almost every place;
• in rank one every finite Hasse sign is trivial, and in rank two s_v(Q) = 1 wherever the image of d(Q) in K_v is the class of -1, since the localization is then a hyperbolic plane.

So the system of a form of positive rank is admissible exactly when its Hasse product is one. For a diagonalization Q ≅ ⟨a₁, …, aₙ⟩ over K, the Hasse product is ∏_{i<j} (∏_v (aᵢ, aⱼ)_v · ∏_w (aᵢ, aⱼ)_w) over the finite places v and real places w, so the product relation follows from the product formula for the Hilbert symbol applied to each pair of coefficients.

Main definitions

• QuadraticForm.globalInvariants: the system of local invariants of a regular global form.

Main results

• QuadraticMap.Equivalent.globalInvariants_eq: isometric forms have the same system.
• QuadraticForm.globalInvariants_realHasse_eq_prod_hilbertSymbol: the real Hasse sign of the system is ∏_{i<j} (aᵢ, aⱼ)_w for any diagonalization.
• QuadraticForm.globalInvariants_hasseProduct_eq_prod: the Hasse product of the system as a product over the pairs of coefficients of a diagonalization.
• QuadraticForm.isAdmissible_globalInvariants_iff: the system is admissible exactly when the rank is positive and the Hasse product is one.
• QuadraticForm.globalInvariants_weightedSumSquares_fin_one: the system of the line ⟨c⟩.
• TauCeti.NumberField.QuadraticForm.globalInvariants_weightedSumSquares_one_self_neg: the system of ⟨1, a, -a⟩ does not depend on a.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 63:20–23 and 66:5–6 for the local invariants and their finite support, and 72:1 for the conditions they satisfy.
• J.-P. Serre, A Course in Arithmetic, Springer (1973), Chapter IV, §3.1 and §3.3, the same invariants and conditions over ℚ.

noncomputable def QuadraticForm.globalInvariants {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) : TauCeti.NumberField.QuadraticForm.GlobalFormInvariants K

The system of local invariants of a regular quadratic form Q over a number field: its rank, its plain discriminant d(Q) ∈ Kˣ/(Kˣ)², its Hasse sign at every finite place and its positive index at every real place.

@[simp]

theorem QuadraticForm.globalInvariants_rank {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) : (Q.globalInvariants hQ).rank = Module.finrank K V

The rank of the system of a form is the dimension of its space.

@[simp]

theorem QuadraticForm.globalInvariants_discr {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) : (Q.globalInvariants hQ).discr = (TauCeti.formClass Q hQ).discr

The discriminant of the system of a form is its plain discriminant.

@[simp]

theorem QuadraticForm.globalInvariants_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) : (Q.globalInvariants hQ).finiteHasse = Q.finiteHasse hQ

The finite Hasse signs of the system of a form are those of the form.

@[simp]

theorem QuadraticForm.globalInvariants_realPositiveIndex {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) : (Q.globalInvariants hQ).realPositiveIndex = Q.realPositiveIndex

The real positive indices of the system of a form are those of the form.

theorem QuadraticForm.globalInvariants_discrAtFinitePlace {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.globalInvariants hQ).discrAtFinitePlace v = (TauCeti.formClass (Q.atFinitePlace v) ⋯).discr

The discriminant of the system of a form at a finite place v is the discriminant of the localization of the form at v.

theorem QuadraticForm.globalInvariants_realNegativeIndex {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) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (Q.globalInvariants hQ).realNegativeIndex w = Q.realNegativeIndex w

The negative index of the system of a form at a real place is that of the form.

theorem QuadraticForm.globalInvariants_realHasse_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))) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (Q.globalInvariants hQ).realHasse w = ∏ i : Fin n, ∏ j > i, TauCeti.hilbertSymbol ((TauCeti.unitAtRealPlace w) (a i)) ((TauCeti.unitAtRealPlace w) (a j))

The real Hasse sign of the system of a form. If Q ≅ ⟨a₁, …, aₙ⟩ over K, the real Hasse sign of the system of Q at a real place w is ∏_{i<j} (aᵢ, aⱼ)_w, the product of the real Hilbert symbols of the images of the coefficients.

theorem QuadraticForm.globalInvariants_hasseProduct_eq_prod {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))) : (Q.globalInvariants hQ).hasseProduct = ∏ i : Fin n, ∏ j > i, (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), TauCeti.hilbertSymbol (v.unitAtFinitePlace (a i)) (v.unitAtFinitePlace (a j))) * ∏ w : { w : NumberField.InfinitePlace K // w.IsReal }, TauCeti.hilbertSymbol ((TauCeti.unitAtRealPlace w) (a i)) ((TauCeti.unitAtRealPlace w) (a j))

The Hasse product of the system of a form, computed on a diagonalization Q ≅ ⟨a₁, …, aₙ⟩ over K: it is the product over the pairs i < j of the products ∏_v (aᵢ, aⱼ)_v · ∏_w (aᵢ, aⱼ)_w of the Hilbert symbols of aᵢ and aⱼ over all finite places v and all real places w.

theorem QuadraticForm.isAdmissible_globalInvariants_iff {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) : (Q.globalInvariants hQ).IsAdmissible ↔ 1 ≤ Module.finrank K V ∧ (Q.globalInvariants hQ).hasseProduct = 1

Admissibility of the system of a form. The system of local invariants of a regular form satisfies every admissibility condition except possibly the positivity of the rank and the product relation, so it is admissible exactly when the rank is positive and the Hasse product is one.

theorem QuadraticForm.globalInvariants_weightedSumSquares_fin_one {K : Type u} [Field K] [NumberField K] (c : Kˣ) (h : QuadraticMap.Nondegenerate) : globalInvariants (QuadraticMap.weightedSumSquares K ![↑c]) h = { rank := 1, discr := TauCeti.squareClass c, finiteHasse := 1, realPositiveIndex := fun (w : { w : NumberField.InfinitePlace K // w.IsReal }) => if 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑c then 1 else 0 }

The local invariants of a line ⟨c⟩: rank one, discriminant the class of c, trivial Hasse sign at every finite place, and positive index 1 or 0 at a real place according to the sign of c there.

theorem QuadraticMap.Equivalent.globalInvariants_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) : Q.globalInvariants hQ = R.globalInvariants hR

Isometric regular forms have the same system of local invariants.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.exists_globalForm_of_globalInvariants_eq {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) {I : GlobalFormInvariants K} (hQI : Q.globalInvariants hQ = I) : ∃ (Q' : QuadraticForm K (Fin I.rank → K)) (hQ' : QuadraticMap.Nondegenerate), Q'.globalInvariants hQ' = I

A system realized by a regular form on some finite-dimensional space is realized by a regular form on the coordinate space Fin I.rank → K.

theorem TauCeti.NumberField.QuadraticForm.globalInvariants_weightedSumSquares_one_self_neg {K : Type u_1} [Field K] [NumberField K] (a : Kˣ) : QuadraticForm.globalInvariants (QuadraticMap.weightedSumSquares K ![1, ↑a, -↑a]) ⋯ = { rank := 3, discr := squareClass (-1), finiteHasse := 1, realPositiveIndex := fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => 2 }

The local invariants of ⟨1⟩ ⊥ ⟨a, -a⟩. Over a number field the system of local invariants of ⟨1, a, -a⟩ does not depend on a: rank 3, discriminant the class of -1, trivial Hasse sign at every finite place, and positive index 2 at every real place.