Weak approximation in local square classes #
A nonzero element of a number field can realize independently prescribed square classes at finitely many finite and real places. The finite-place statement includes dyadic places. This is the coefficientwise approximation needed to construct quadratic forms with prescribed local behavior.
References #
- O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 72:1.
theorem
TauCeti.GlobalNumberFields.exists_fieldUnit_isSquare_div_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 : (v : ↥S) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)ˣ)
(b : ↥T → ℝˣ)
:
∃ (x : Kˣ),
(∀ (v : ↥S), IsSquare ((algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)) ↑x / ↑(a v))) ∧ ∀ (w : ↥T), IsSquare ((NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑x / ↑(b w))
One global field unit realizes any prescribed square classes at finitely many finite and real places. The quotients are read in the actual completions and in the real embeddings.
theorem
TauCeti.GlobalNumberFields.exists_coefficients_prod_eq_isSquare_div_at_places
{K : Type u_1}
[Field K]
[NumberField K]
{n : ℕ}
(S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)))
(T : Finset { w : NumberField.InfinitePlace K // w.IsReal })
(d : Kˣ)
(a : (v : ↥S) → Fin (n + 1) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)ˣ)
(b : ↥T → Fin (n + 1) → ℝˣ)
(ha :
∀ (v : ↥S),
IsSquare
((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v))) d / ∏ i : Fin (n + 1), a v i))
(hb :
∀ (w : ↥T), IsSquare ((Units.map ↑(NumberField.InfinitePlace.embedding_of_isReal ⋯)) d / ∏ i : Fin (n + 1), b w i))
:
∃ (c : Fin (n + 1) → Kˣ),
∏ i : Fin (n + 1), c i = d ∧ (∀ (v : ↥S) (i : Fin (n + 1)),
IsSquare ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v))) (c i) / a v i)) ∧ ∀ (w : ↥T) (i : Fin (n + 1)),
IsSquare ((Units.map ↑(NumberField.InfinitePlace.embedding_of_isReal ⋯)) (c i) / b w i)
Local coefficient square classes whose products agree with a global unit can be realized by global coefficients whose product is exactly that unit.