Systems of local invariants of global quadratic forms

A regular quadratic form of rank n over a number field K has the following invariants:

• its rank n;
• its plain discriminant d ∈ Kˣ/(Kˣ)², one global square class;
• at each finite place v, its Hasse sign s_v = ∏_{i<j} (a_i, a_j)_v ∈ {±1};
• at each real place w, its positive index p_w.

This file defines the carrier GlobalFormInvariants K of such data, with no reference to a form, and the predicate GlobalFormInvariants.IsAdmissible cutting out the systems that can arise from a form. Admissibility consists of the exact conditions:

1. 1 ≤ n;
2. at every real place p_w ≤ n, and the image of d in ℝˣ/(ℝˣ)² is the class of (-1)^(n - p_w);
3. s_v = 1 at all but finitely many finite places;
4. in rank one s_v = 1, and in rank two s_v = 1 wherever the image of d in K_v is the class of -1;
5. the product of all s_v and of the real Hasse signs (-1)^((n - p_w)(n - p_w - 1)/2) is 1.

The global discriminant is part of the carrier, and only its images are read at the places: the local discriminants of a system are not independent data. Condition 4 records the two local triples (n, d_v, s_v) over a nonarchimedean local field that no regular form realizes: a form of rank one has trivial Hasse sign, and a binary form of discriminant -1 is a hyperbolic plane, whose Hasse sign is also trivial. Neither exception follows from the others, as the rank-one and rank-two families below show: with Hasse sign -1 at exactly two finite places they have finite support and total product one, and are still not admissible.

Main definitions

• TauCeti.NumberField.QuadraticForm.GlobalFormInvariants: rank, global discriminant, finite Hasse signs and real positive indices.
• GlobalFormInvariants.discrAtFinitePlace, GlobalFormInvariants.discrAtRealPlace: the images of the global discriminant in the completions.
• GlobalFormInvariants.realNegativeIndex, GlobalFormInvariants.realHasse: the negative index n - p_w and the Hasse sign (-1)^((n - p_w)(n - p_w - 1)/2) at a real place.
• GlobalFormInvariants.hasseProduct: the product of all finite and real Hasse signs.
• GlobalFormInvariants.IsAdmissible: the admissibility conditions above.

Main results

• GlobalFormInvariants.hasseProduct_eq_prod_of_mulSupport_subset: the Hasse product may be computed over any finite set of finite places containing the support of the Hasse signs.
• GlobalFormInvariants.hasseProduct_eq_neg_one_pow_card: with Hasse sign -1 exactly on a finite set T of finite places and trivial real Hasse signs, the Hasse product is (-1)^#T.
• GlobalFormInvariants.isAdmissible_positiveDefinite_iff_even_card: in rank at least three, the positive-definite system of trivial discriminant with Hasse sign -1 exactly on T is admissible exactly when #T is even.
• GlobalFormInvariants.isAdmissible_rankOne_iff_eq_empty, GlobalFormInvariants.isAdmissible_rankTwo_iff_eq_empty: the corresponding systems in rank one, and in rank two with discriminant -1, are admissible only for T = ∅, although for every even T their Hasse product is one.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 63:20–23 for the local realization exceptions and 72:1 for existence with prescribed local invariants.
• J.-P. Serre, A Course in Arithmetic, Springer (1973), Chapter IV, §3.3, Theorem 9, the same conditions over ℚ.

structure TauCeti.NumberField.QuadraticForm.GlobalFormInvariants (K : Type u_1) [Field K] [NumberField K] : Type u_1

A system of local invariants of a quadratic form over a number field K: a rank n, a global plain discriminant d ∈ Kˣ/(Kˣ)², a Hasse sign s_v ∈ {±1} at every finite place v, and a positive index p_w at every real place w. No condition relates the data; the systems arising from regular forms of positive rank are those satisfying IsAdmissible.

• rank : ℕ

  The rank n.

• discr : SquareClassGroup K

  The global plain discriminant d ∈ Kˣ/(Kˣ)².

• finiteHasse : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) → ℤˣ

  The Hasse sign s_v ∈ {±1} at a finite place v.

• realPositiveIndex : { w : NumberField.InfinitePlace K // w.IsReal } → ℕ

  The positive index p_w at a real place w.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.ext {K : Type u_1} {inst✝ : Field K} {inst✝¹ : NumberField K} {x y : GlobalFormInvariants K} (rank : x.rank = y.rank) (discr : x.discr = y.discr) (finiteHasse : x.finiteHasse = y.finiteHasse) (realPositiveIndex : x.realPositiveIndex = y.realPositiveIndex) : x = y

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.ext_iff {K : Type u_1} {inst✝ : Field K} {inst✝¹ : NumberField K} {x y : GlobalFormInvariants K} : x = y ↔ x.rank = y.rank ∧ x.discr = y.discr ∧ x.finiteHasse = y.finiteHasse ∧ x.realPositiveIndex = y.realPositiveIndex

noncomputable def TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.discrAtFinitePlace {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : SquareClassGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

The discriminant of a system at a finite place v: the image of the global discriminant in K_vˣ/(K_vˣ)².

@[simp]

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.discrAtFinitePlace_def {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : I.discrAtFinitePlace v = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap I.discr

Unfolds discrAtFinitePlace.

noncomputable def TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.discrAtRealPlace {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : SquareClassGroup ℝ

The discriminant of a system at a real place w: the image of the global discriminant in ℝˣ/(ℝˣ)² under the real embedding of w.

@[simp]

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.discrAtRealPlace_def {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : I.discrAtRealPlace w = (NumberField.InfinitePlace.embedding_of_isReal ⋯).squareClassMap I.discr

Unfolds discrAtRealPlace.

def TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.realNegativeIndex {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : ℕ

The negative index n - p_w of a system at a real place w.

@[simp]

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.realNegativeIndex_def {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : I.realNegativeIndex w = I.rank - I.realPositiveIndex w

Unfolds realNegativeIndex.

def TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.realHasse {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : ℤˣ

The Hasse sign of a system at a real place w: (-1)^(q(q-1)/2) for the negative index q = n - p_w, the Hasse sign of the real diagonal form p_w⟨1⟩ ⊥ q⟨-1⟩.

@[simp]

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.realHasse_def {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : I.realHasse w = (-1) ^ (I.realNegativeIndex w).choose 2

Unfolds realHasse.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.realHasse_ne_one_iff_realPositiveIndex_eq_zero_of_rank_eq_two {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (hn : I.rank = 2) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : I.realHasse w ≠ 1 ↔ I.realPositiveIndex w = 0

In rank two, the real Hasse sign is nontrivial exactly when the positive index is zero.

noncomputable def TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.hasseProduct {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) : ℤˣ

The Hasse product of a system: the product of its Hasse signs over all finite places and all real places. The finite factor is a finprod; it is the product of the Hasse signs when they have finite support, which is part of admissibility.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.hasseProduct_def {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) : I.hasseProduct = (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), I.finiteHasse v) * ∏ w : { w : NumberField.InfinitePlace K // w.IsReal }, I.realHasse w

Unfolds hasseProduct.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.hasseProduct_eq_prod_of_mulSupport_subset {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : Function.mulSupport I.finiteHasse ⊆ ↑S) : I.hasseProduct = (∏ v ∈ S, I.finiteHasse v) * ∏ w : { w : NumberField.InfinitePlace K // w.IsReal }, I.realHasse w

The Hasse product is independent of the chosen finite support: it is the product of the finite Hasse signs over any finite set of finite places outside which they are trivial, times the real Hasse signs.

structure TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsAdmissible {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) : Prop

Admissibility of a system of local invariants. A system (n, d, s, p) is admissible when 1 ≤ n; at every real place p_w ≤ n and the image of d is the class of (-1)^(n - p_w); the finite Hasse signs are trivial at almost every place; in rank one every s_v is trivial, and in rank two s_v is trivial wherever the image of d in K_v is the class of -1; and the product of all finite and real Hasse signs is one. These are the systems realized by regular forms of positive rank.

• one_le_rank : 1 ≤ I.rank

  The rank is positive.

• realPositiveIndex_le_rank (w : { w : NumberField.InfinitePlace K // w.IsReal }) : I.realPositiveIndex w ≤ I.rank

  At a real place the positive index is at most the rank.

• discrAtRealPlace_eq (w : { w : NumberField.InfinitePlace K // w.IsReal }) : I.discrAtRealPlace w = I.realNegativeIndex w • squareClass (-1)

  At a real place the discriminant is the class of (-1)^(n - p_w).

• hasFiniteMulSupport_finiteHasse : Function.HasFiniteMulSupport I.finiteHasse

  The finite Hasse signs are trivial at almost every finite place.

• finiteHasse_eq_one_of_rank_eq_one (hn : I.rank = 1) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : I.finiteHasse v = 1

  In rank one every finite Hasse sign is trivial.

• finiteHasse_eq_one_of_rank_eq_two (hn : I.rank = 2) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hd : I.discrAtFinitePlace v = squareClass (-1)) : I.finiteHasse v = 1

  In rank two the finite Hasse sign is trivial where the discriminant is the class of -1.

• hasseProduct_eq_one : I.hasseProduct = 1

  The product of all finite and real Hasse signs is one.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsAdmissible.realPositiveIndex_add_realNegativeIndex_eq_rank {K : Type u_1} [Field K] [numberFieldK : NumberField K] {I : GlobalFormInvariants K} (hI : I.IsAdmissible) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : I.realPositiveIndex w + I.realNegativeIndex w = I.rank

At a real place of an admissible system, the positive and negative indices add up to the rank.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsAdmissible.prod_finiteHasse_mul_prod_realHasse_eq_one {K : Type u_1} [Field K] [numberFieldK : NumberField K] {I : GlobalFormInvariants K} (hI : I.IsAdmissible) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : Function.mulSupport I.finiteHasse ⊆ ↑S) : (∏ v ∈ S, I.finiteHasse v) * ∏ w : { w : NumberField.InfinitePlace K // w.IsReal }, I.realHasse w = 1

For an admissible system, the product of its finite Hasse signs over any finite set of finite places outside which they are trivial, times its real Hasse signs, is one.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsAdmissible.embedding_of_isReal_neg_iff_odd {K : Type u_1} [Field K] [numberFieldK : NumberField K] {I : GlobalFormInvariants K} (hI : I.IsAdmissible) {d : Kˣ} (hd : squareClass d = I.discr) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑d < 0 ↔ Odd (I.realNegativeIndex w)

At a real place of an admissible system, a representative d of the discriminant is negative exactly when the negative index is odd.

Hasse signs -1 on a finite set of places

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.hasseProduct_eq_neg_one_pow_card {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hs : I.finiteHasse = (↑T).mulIndicator fun (x : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => -1) (hr : ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), I.realHasse w = 1) : I.hasseProduct = (-1) ^ T.card

The Hasse product of a system with Hasse sign -1 exactly at the finite places of T and trivial real Hasse signs is (-1)^#T.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.forall_finiteHasse_eq_one_iff_eq_empty {K : Type u_1} [Field K] [numberFieldK : NumberField K] (I : GlobalFormInvariants K) (T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hs : I.finiteHasse = (↑T).mulIndicator fun (x : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => -1) : (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), I.finiteHasse v = 1) ↔ T = ∅

A system with Hasse sign -1 exactly at the finite places of T has all finite Hasse signs trivial exactly when T is empty.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.isAdmissible_positiveDefinite_iff_even_card {K : Type u_1} [Field K] [numberFieldK : NumberField K] (T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) {n : ℕ} (hn : 3 ≤ n) : { rank := n, discr := 0, finiteHasse := (↑T).mulIndicator fun (x : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => -1, realPositiveIndex := fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => n }.IsAdmissible ↔ Even T.card

The positive-definite systems of trivial discriminant. In rank n ≥ 3, the system with trivial global discriminant, positive index n at every real place and Hasse sign -1 exactly at the finite places of T is admissible exactly when T has even cardinality.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.isAdmissible_rankOne_iff_eq_empty {K : Type u_1} [Field K] [numberFieldK : NumberField K] (T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : { rank := 1, discr := 0, finiteHasse := (↑T).mulIndicator fun (x : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => -1, realPositiveIndex := fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => 1 }.IsAdmissible ↔ T = ∅

The rank-one exception. The rank-one system with trivial discriminant, positive index 1 at every real place and Hasse sign -1 exactly at the finite places of T is admissible only for T = ∅, although its Hasse signs have finite support and, for #T even, product one (hasseProduct_eq_neg_one_pow_card).

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.isAdmissible_rankTwo_iff_eq_empty {K : Type u_1} [Field K] [numberFieldK : NumberField K] (T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : { rank := 2, discr := squareClass (-1), finiteHasse := (↑T).mulIndicator fun (x : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => -1, realPositiveIndex := fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => 1 }.IsAdmissible ↔ T = ∅

The rank-two exception. The rank-two system with discriminant the class of -1, positive index 1 at every real place and Hasse sign -1 exactly at the finite places of T is admissible only for T = ∅, although its Hasse signs have finite support and, for #T even, product one (hasseProduct_eq_neg_one_pow_card).