Discriminants of localized quadratic forms

The discriminant of a regular quadratic form over a number field localizes to the image of its global discriminant at every finite place and along every real or complex embedding.

Thus the discriminant attached to an actual localized form agrees with the square class obtained by applying the corresponding place map to the global invariant.

At a real place the real square class of the global discriminant is a sign, and it is determined by the signature there: it is (-1)^q for the negative index q = n - p of the localized form of rank n and positive index p.

@[simp]

theorem QuadraticForm.discr_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) (place : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : have hQv := ⋯; (TauCeti.formClass (Q.atFinitePlace place) hQv).discr = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K place)).squareClassMap (TauCeti.formClass Q hQ).discr

At a finite place, the discriminant of the localized form is the image of its global discriminant.

@[simp]

theorem QuadraticForm.discr_atRealPlace {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) (place : { w : NumberField.InfinitePlace K // w.IsReal }) : have hQw := ⋯; (TauCeti.formClass (Q.atRealPlace place) hQw).discr = (NumberField.InfinitePlace.embedding_of_isReal ⋯).squareClassMap (TauCeti.formClass Q hQ).discr

At a real place, the discriminant of the localized form is the image of its global discriminant under the place's real embedding.

@[simp]

theorem QuadraticForm.discr_atComplexEmbedding {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) (place : NumberField.InfinitePlace K) : have hQw := ⋯; (TauCeti.formClass (Q.atComplexEmbedding place) hQw).discr = place.embedding.squareClassMap (TauCeti.formClass Q hQ).discr

Along a complex embedding, the discriminant of the scalar extension is the image of its global discriminant.

theorem QuadraticForm.squareClassMap_discr_formClass_eq_realNegativeIndex_nsmul {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) (place : { w : NumberField.InfinitePlace K // w.IsReal }) : (NumberField.InfinitePlace.embedding_of_isReal ⋯).squareClassMap (TauCeti.formClass Q hQ).discr = Q.realNegativeIndex place • TauCeti.squareClass (-1)

At a real place, the image of the global discriminant is the class of (-1)^q, where q is the negative index of the form at that place.

theorem QuadraticForm.squareClassMap_discr_formClass_eq_finrank_sub_realPositiveIndex_nsmul {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) (place : { w : NumberField.InfinitePlace K // w.IsReal }) : (NumberField.InfinitePlace.embedding_of_isReal ⋯).squareClassMap (TauCeti.formClass Q hQ).discr = (Module.finrank K V - Q.realPositiveIndex place) • TauCeti.squareClass (-1)

At a real place, the image of the global discriminant of a form of rank n and positive index p is the class of (-1)^(n - p).

@[simp]

theorem QuadraticForm.squareClassMap_discr_formClass_eq_zero_iff_even_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) (place : { w : NumberField.InfinitePlace K // w.IsReal }) : (NumberField.InfinitePlace.embedding_of_isReal ⋯).squareClassMap (TauCeti.formClass Q hQ).discr = 0 ↔ Even (Q.realNegativeIndex place)

At a real place, the image of the global discriminant is trivial exactly when the negative index of the form at that place is even.