Approximating local quadratic forms with a fixed discriminant

Given regular forms of the same positive rank at finitely many finite and real places of a number field, with discriminants induced by one global square class, there is a regular global form with that discriminant isometric to all the prescribed forms. There is no condition on Hasse signs away from the selected places.

This is the initial approximation in the construction of a form with prescribed local behavior. The global diagonal coefficients have product equal to a chosen representative of the discriminant: the first coefficients are chosen in the prescribed local square classes, and the last coefficient is determined by their product.

References

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

theorem TauCeti.NumberField.QuadraticForm.exists_form_discr_eq_equivalent_at_places {K : Type u_1} [Field K] [NumberField K] {n : ℕ} (hn : 0 < n) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (T : Finset { w : NumberField.InfinitePlace K // w.IsReal }) (d : Kˣ) (U : (v : ↥S) → QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v) (Fin n → IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)) (R : ↥T → QuadraticForm ℝ (Fin n → ℝ)) (hU : ∀ (v : ↥S), QuadraticMap.Nondegenerate) (hR : ∀ (w : ↥T), QuadraticMap.Nondegenerate) (hUd : ∀ (v : ↥S), have this := invertibleOfNonzero ⋯; have this := (Invertible.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)) 2).copy 2 ⋯; (formClass (U v) ⋯).discr = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)).squareClassMap (squareClass d)) (hRd : ∀ (w : ↥T), (formClass (R w) ⋯).discr = (NumberField.InfinitePlace.embedding_of_isReal ⋯).squareClassMap (squareClass d)) : ∃ (Q : QuadraticForm K (Fin n → K)) (hQ : QuadraticMap.Nondegenerate), (formClass Q hQ).discr = squareClass d ∧ (∀ (v : ↥S), QuadraticMap.Equivalent (Q.atFinitePlace ↑v) (U v)) ∧ ∀ (w : ↥T), QuadraticMap.Equivalent (Q.atRealPlace ↑w) (R w)

Regular local forms of the same positive rank and with discriminants induced by one global unit can be matched at finitely many places by a regular global form of that discriminant.