A global nonsquare at prescribed places

For finitely many finite and real places of a number field, one field element is a nonsquare in every corresponding completion. At a finite place its valuation is prescribed to be one; at a real place its image is negative. At every other real place it is positive, hence a square. The simultaneous choice uses weak approximation.

This supplies the radicand in the unprescribed form of Hilbert sign prescription: at each selected place the associated quadratic extension is a field rather than a split algebra. With no real place selected, it supplies the radicand β of the correction planes ⟨1, -β⟩ and ⟨α, -αβ⟩ in the construction of a form with prescribed local behavior, which must be a square at every archimedean place.

References

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

theorem TauCeti.NumberField.QuadraticForm.exists_fieldUnit_not_isSquare_at_places {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (T : Finset { w : NumberField.InfinitePlace K // w.IsReal }) : ∃ (a : Kˣ), (∀ v ∈ S, (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑a = WithZero.exp (-1) ∧ ¬IsSquare (v.unitAtFinitePlace a)) ∧ (∀ w ∈ T, (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑a < 0 ∧ ¬IsSquare ((unitAtRealPlace w) a)) ∧ ∀ w ∉ T, 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑a

Given finite sets of finite and real places, there is one global unit that is a nonsquare in each of their completions. At each selected finite place it has valuation one, at each selected real place it is negative, and at every other real place it is positive.