Global forms with prescribed local behavior, up to one representation

Let I be an admissible system of local invariants of rank n over a number field K, and let U_v (at the finite places) and R_w (at the real places) be regular local forms realizing I. O'Meara's existence theorem 72:1 produces a regular global form isometric to U_v and R_w at every place. This file carries out its construction up to the one step that needs the local-global principle for representations.

1. A regular global form W of rank n with the global discriminant of I is chosen isometric to R_w at every real place, by approximating diagonal coefficients.
2. The finite places where W_v and U_v are not isometric are those where their Hasse signs differ. There are finitely many of them, and an even number, because both Hasse products are one and the real Hasse signs agree.
3. Weak approximation gives β ∈ Kˣ positive at every real place and a nonsquare at each of these places, and Hilbert sign prescription gives α ∈ Kˣ with (α, β)_v = -1 exactly there.

So W_v ≅ U_v exactly when (α, β)_v = 1. With the correction planes P = ⟨1, -β⟩ and P' = ⟨α, -αβ⟩, the plane P' is then represented by P ⊥ W at every finite and real place, and any representation of P' by P ⊥ W over K yields a regular global form whose system of local invariants is I.

The Hasse product formula for W is Hilbert reciprocity (QuadraticForm.globalInvariants_hasseProduct_eq_one), and the choice of α is Hilbert sign prescription (TauCeti.NumberField.QuadraticForm.exists_hilbertSymbol_eq_ite), so both steps hold over every number field.

Main results

Both results are in the namespace TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.

• IsLocalRealization.exists_atFinitePlace_equivalent_iff_hilbertSymbol_eq_one: a first global approximation W and elements α, β with W_v ≅ U_v ↔ (α, β)_v = 1 at every finite place, W_w ≅ R_w at every real place and β positive at every real place.
• IsLocalRealization.exists_locallyRepresents_prod: ⟨α, -αβ⟩ is locally represented by ⟨1, -β⟩ ⊥ W, and a global representation gives a regular global form whose system of local invariants is I.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 72:1, with 71:19a for the choice of α.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.exists_atFinitePlace_equivalent_iff_hilbertSymbol_eq_one {K : Type u_1} [Field K] [NumberField K] {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 → ℝ)} (hI : I.IsAdmissible) (hL : I.IsLocalRealization U R) : ∃ (W : QuadraticForm K (Fin I.rank → K)) (hW : QuadraticMap.Nondegenerate) (a : Kˣ) (b : Kˣ), (formClass W hW).discr = I.discr ∧ (∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), QuadraticMap.Equivalent (W.atRealPlace w) (R w)) ∧ (∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b) ∧ ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Equivalent (W.atFinitePlace v) (U v) ↔ hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b) = 1

The approximation and correction data of O'Meara 72:1. Let U_v and R_w be local forms realizing an admissible system I. Then there are a regular global form W of rank I.rank with the global discriminant of I, isometric to R_w at every real place, and α, β ∈ Kˣ, with β positive at every real place, such that W_v ≅ U_v exactly when (α, β)_v = 1, at every finite place v.

theorem TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.exists_locallyRepresents_prod {K : Type u_1} [Field K] [NumberField K] {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 → ℝ)} (hI : I.IsAdmissible) (hL : I.IsLocalRealization U R) : ∃ (W : QuadraticForm K (Fin I.rank → K)) (_ : QuadraticMap.Nondegenerate) (a : Kˣ) (b : Kˣ), QuadraticForm.LocallyRepresents (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W) ∧ ((QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]).IsRepresentedBy ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W) → ∃ (Q : QuadraticForm K (Fin I.rank → K)) (hQ : QuadraticMap.Nondegenerate), Q.globalInvariants hQ = I)

O'Meara 72:1 up to one global representation. Let U_v and R_w be local forms realizing an admissible system I. Then there are a regular global form W of rank I.rank and α, β ∈ Kˣ such that ⟨α, -αβ⟩ is represented by ⟨1, -β⟩ ⊥ W at every finite and real place, and such that, if ⟨α, -αβ⟩ is represented by ⟨1, -β⟩ ⊥ W over K, some regular global form on K ^ I.rank has I as its system of local invariants.