Parity of finite Hasse discrepancies

Two systems of local invariants satisfying the Hasse product relation and having the same real Hasse signs differ at an even number of finite places. This supplies the parity condition on the finite correction set in the construction of a global form with prescribed local invariants.

The statement uses a finite set containing both supports, so it applies without making a choice of support. The filtered set is exactly the set of finite places where the two signs differ.

Reference

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 72:1.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.even_card_finiteHasse_ne {K : Type u_1} [Field K] [NumberField K] (I J : GlobalFormInvariants K) (hI : I.hasseProduct = 1) (hJ : J.hasseProduct = 1) (hreal : ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), I.realHasse w = J.realHasse w) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hSI : Function.mulSupport I.finiteHasse ⊆ ↑S) (hSJ : Function.mulSupport J.finiteHasse ⊆ ↑S) : Even {v ∈ S | I.finiteHasse v ≠ J.finiteHasse v}.card

If two systems have Hasse product one and equal real Hasse signs, the number of finite places at which their finite Hasse signs differ is even. The finite set S may contain extra places, since these are removed by the filter.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.exists_even_finiteHasse_discrepancy {K : Type u_1} [Field K] [NumberField K] (I J : GlobalFormInvariants K) (hI : I.IsAdmissible) (hJ : J.IsAdmissible) (hreal : ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), I.realHasse w = J.realHasse w) : ∃ (R : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))), (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), v ∈ R ↔ I.finiteHasse v ≠ J.finiteHasse v) ∧ Even R.card

The finite places where two admissible systems with equal real Hasse signs disagree form an even finite set. The returned set is characterized by membership, independently of the supports used to calculate it.