Local classification of quadratic forms over a number field

Over a nonarchimedean local field, regular quadratic forms are classified by their rank, plain discriminant and local Hasse invariant (QuadraticForm.equivalent_iff_finrank_eq_and_discr_eq_and_localHasse_eq). This file restates that classification at a finite place v of a number field K in terms of the invariants of a global regular form Q: the rank of the localization Q_v is the rank of Q, its discriminant is the image in K_vˣ/(K_vˣ)² of the global discriminant d(Q), and its local Hasse invariant is the finite Hasse sign s_v(Q). So Q_v is isometric to a regular form U over K_v exactly when these three invariants match those of U, and two localizations Q_v and R_v are isometric exactly when Q and R have the same rank, the same discriminant at v and the same Hasse sign at v.

Combined with Sylvester's law at the real places, this characterizes local equivalence (at every finite and real place) by the rank, the discriminants at the finite places, the finite Hasse signs and the real positive indices. The criterion uses the discriminant at each finite place rather than the global discriminant: that two forms with the same discriminant at every place have the same global discriminant is the global square theorem. In particular, forms with the same system of local invariants QuadraticForm.globalInvariants are locally equivalent, and a global form whose system is I is isometric at every finite and real place to each family of local forms realizing I.

In global notation, the two exceptions of the local realization theorem TauCeti.RegularFormClass.exists_of_realization are the small-rank conditions of TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsAdmissible.

Main results

• formClass_atFinitePlace: the class of the localization of a form at a finite place is the scalar extension of the class of the form.
• atFinitePlace_equivalent_iff_finrank_eq_and_discr_eq_and_finiteHasse_eq: the localization of a global form at a finite place is isometric to a regular local form exactly when their ranks, discriminants and Hasse invariants agree.
• equivalent_atFinitePlace_iff_finrank_eq_and_discr_eq_and_finiteHasse_eq: two localizations at a finite place are isometric exactly when the ranks, the discriminants at that place and the finite Hasse signs agree.
• locallyEquivalent_iff_finrank_eq_and_discr_eq_and_finiteHasse_eq_and_realPositiveIndex_eq: two regular forms are locally equivalent exactly when their ranks, their discriminants at every finite place, their finite Hasse signs and their real positive indices agree.
• QuadraticForm.LocallyEquivalent.of_globalInvariants_eq: forms with the same system of local invariants are locally equivalent.
• GlobalFormInvariants.IsLocalRealization.equivalent_atFinitePlace, GlobalFormInvariants.IsLocalRealization.equivalent_atRealPlace: a form whose system is I is isometric at every finite and real place to any family realizing I.
• GlobalFormInvariants.IsLocalRealization.atFinitePlace_equivalent_iff_finiteHasse_eq: a form with the rank and global discriminant of I is isometric at a finite place to a family realizing I exactly when its Hasse sign there is the prescribed one.
• GlobalFormInvariants.IsLocalRealization.atRealPlace_equivalent_iff_realPositiveIndex_eq: a form of rank I.rank is isometric at a real place to a family realizing I exactly when its positive index there is the prescribed one.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 63:20 for the local classification and 66:5 for the local invariants of a global form.
• J.-P. Serre, A Course in Arithmetic, Springer (1973), Chapter IV, §2.3, Theorem 7, and §3.1.

theorem QuadraticForm.formClass_atFinitePlace {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)) : TauCeti.formClass (Q.atFinitePlace v) ⋯ = TauCeti.RegularFormClass.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TauCeti.formClass Q hQ)

The class of the localization of a form at a finite place is the scalar extension of the class of the form.

theorem QuadraticForm.atFinitePlace_equivalent_iff_finrank_eq_and_discr_eq_and_finiteHasse_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) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {X : Type u_1} [AddCommGroup X] [Module (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) X] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) X] {U : QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) X} (hU : QuadraticMap.Nondegenerate) : QuadraticMap.Equivalent (Q.atFinitePlace v) U ↔ Module.finrank K V = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) X ∧ (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass Q hQ).discr = (TauCeti.formClass U hU).discr ∧ Q.finiteHasse hQ v = (TauCeti.formClass U hU).localHasse

Local classification at a finite place, in global notation. The localization of a regular form Q at a finite place v is isometric to a regular form U over K_v exactly when the rank of Q is the dimension of U, the image of the global discriminant of Q in K_vˣ/(K_vˣ)² is the discriminant of U, and the finite Hasse sign s_v(Q) is the local Hasse invariant of U.

theorem QuadraticForm.equivalent_atFinitePlace_iff_finrank_eq_and_discr_eq_and_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) (hQ : QuadraticMap.Nondegenerate) (R : QuadraticForm K W) (hR : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : QuadraticMap.Equivalent (Q.atFinitePlace v) (R.atFinitePlace v) ↔ Module.finrank K V = Module.finrank K W ∧ (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 ∧ Q.finiteHasse hQ v = R.finiteHasse hR v

Local classification at a finite place. The localizations of two regular forms Q and R at a finite place v are isometric exactly when Q and R have the same rank, the images of their global discriminants in K_vˣ/(K_vˣ)² agree, and their finite Hasse signs at v agree.

theorem QuadraticForm.locallyEquivalent_iff_finrank_eq_and_discr_eq_and_finiteHasse_eq_and_realPositiveIndex_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} (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate) : Q.LocallyEquivalent R ↔ Module.finrank K V = Module.finrank K W ∧ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (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) ∧ Q.finiteHasse hQ = R.finiteHasse hR ∧ Q.realPositiveIndex = R.realPositiveIndex

Local equivalence by invariants. Two regular forms over a number field are isometric at every finite and every real place exactly when they have the same rank, the images of their global discriminants agree at every finite place, and they have the same Hasse sign at every finite place and the same positive index at every real place.

theorem QuadraticForm.LocallyEquivalent.of_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} {hQ : QuadraticMap.Nondegenerate} {hR : QuadraticMap.Nondegenerate} (h : Q.globalInvariants hQ = R.globalInvariants hR) : Q.LocallyEquivalent R

Regular forms with the same system of local invariants are isometric at every finite and every real place.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.equivalent_atFinitePlace {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {I : GlobalFormInvariants K} {U : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (Fin I.rank → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {R : { w : NumberField.InfinitePlace K // w.IsReal } → QuadraticForm ℝ (Fin I.rank → ℝ)} {Q : QuadraticForm K V} {hQ : QuadraticMap.Nondegenerate} (hL : I.IsLocalRealization U R) (hQI : Q.globalInvariants hQ = I) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : QuadraticMap.Equivalent (Q.atFinitePlace v) (U v)

A regular form whose system of local invariants is I is isometric at every finite place v to the form at v of any family realizing I.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.atFinitePlace_equivalent_iff_finiteHasse_eq {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {I : GlobalFormInvariants K} {U : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (Fin I.rank → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {R : { w : NumberField.InfinitePlace K // w.IsReal } → QuadraticForm ℝ (Fin I.rank → ℝ)} {Q : QuadraticForm K V} {hQ : QuadraticMap.Nondegenerate} (hL : I.IsLocalRealization U R) (hQr : Module.finrank K V = I.rank) (hQd : (formClass Q hQ).discr = I.discr) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : QuadraticMap.Equivalent (Q.atFinitePlace v) (U v) ↔ Q.finiteHasse hQ v = I.finiteHasse v

A regular form of rank I.rank with the global discriminant of I is isometric at a finite place v to the form at v of a family realizing I exactly when its Hasse sign at v is the prescribed one.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.atRealPlace_equivalent_iff_realPositiveIndex_eq {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {I : GlobalFormInvariants K} {U : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (Fin I.rank → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {R : { w : NumberField.InfinitePlace K // w.IsReal } → QuadraticForm ℝ (Fin I.rank → ℝ)} {Q : QuadraticForm K V} (hL : I.IsLocalRealization U R) (hQ : QuadraticMap.Nondegenerate) (hQr : Module.finrank K V = I.rank) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Equivalent (Q.atRealPlace w) (R w) ↔ Q.realPositiveIndex w = I.realPositiveIndex w

A regular form of rank I.rank is isometric at a real place w to the form at w of a family realizing I exactly when its positive index at w is the prescribed one.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.equivalent_atRealPlace {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {I : GlobalFormInvariants K} {U : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (Fin I.rank → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {R : { w : NumberField.InfinitePlace K // w.IsReal } → QuadraticForm ℝ (Fin I.rank → ℝ)} {Q : QuadraticForm K V} {hQ : QuadraticMap.Nondegenerate} (hL : I.IsLocalRealization U R) (hQI : Q.globalInvariants hQ = I) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Equivalent (Q.atRealPlace w) (R w)

A regular form whose system of local invariants is I is isometric at every real place w to the form at w of any family realizing I.