Weak approximation for vectors at finite and real places

Let K be a number field and V a finite-dimensional K-vector space. For finitely many finite places v and real places w, one global vector x : V can be chosen so that its images 1 ⊗ x in the localized spaces K_v ⊗[K] V and ℝ ⊗[K] V lie in arbitrarily prescribed neighbourhoods of arbitrary local vectors. The real spaces are the scalar extensions along the embedding of the real place, exactly as in the localization of quadratic forms.

The localized spaces carry no topology of their own. The results here assume only that each one carries its module topology (IsModuleTopology), which is the topology of coordinates with respect to any basis. The statements are therefore independent of a choice of basis, and they apply to moduleTopology as well as to the usual topology of a finite-dimensional real vector space.

These results are the vector form of the scalar statement GlobalNumberFields.denseRange_algebraMap_embedding_of_isReal, Artin--Whaples weak approximation at finite and real places, which is the case V = K.

This is the form of weak approximation used to approximate vectors of a quadratic space, such as the coordinates of a vector in a binary summand in the proof of the Hasse--Minkowski theorem.

Main results

• TauCeti.NumberField.denseRange_one_tmul: V is dense in the corresponding product of localized spaces.
• TauCeti.NumberField.exists_one_tmul_mem_of_mem_nhds: one global vector lies in prescribed neighbourhoods at finitely many finite and real places.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1973), §66, where weak approximation of vectors enters the proof of the Hasse--Minkowski theorem.
• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, for weak approximation in a number field.

theorem TauCeti.NumberField.denseRange_one_tmul {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (T : Finset { w : NumberField.InfinitePlace K // w.IsReal }) [(v : ↥S) → TopologicalSpace (↑v).FiniteScalarExtension] [∀ (v : ↥S), IsModuleTopology (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v) (↑v).FiniteScalarExtension] [(w : ↥T) → TopologicalSpace (RealScalarExtension ↑w)] [∀ (w : ↥T), IsModuleTopology ℝ (RealScalarExtension ↑w)] : DenseRange fun (x : V) => (fun (v : ↥S) => 1 ⊗ₜ[K] x, fun (w : ↥T) => 1 ⊗ₜ[K] x)

Vector weak approximation. A finite-dimensional vector space over a number field is dense in the product of its scalar extensions to finitely many finite completions and to ℝ along finitely many real places, for the module topologies on those scalar extensions.

theorem TauCeti.NumberField.exists_one_tmul_mem_of_mem_nhds {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (T : Finset { w : NumberField.InfinitePlace K // w.IsReal }) [(v : ↥S) → TopologicalSpace (↑v).FiniteScalarExtension] [∀ (v : ↥S), IsModuleTopology (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v) (↑v).FiniteScalarExtension] [(w : ↥T) → TopologicalSpace (RealScalarExtension ↑w)] [∀ (w : ↥T), IsModuleTopology ℝ (RealScalarExtension ↑w)] {y : (v : ↥S) → (↑v).FiniteScalarExtension} {z : (w : ↥T) → RealScalarExtension ↑w} {N : (v : ↥S) → Set (↑v).FiniteScalarExtension} {M : (w : ↥T) → Set (RealScalarExtension ↑w)} (hN : ∀ (v : ↥S), N v ∈ nhds (y v)) (hM : ∀ (w : ↥T), M w ∈ nhds (z w)) : ∃ (x : V), (∀ (v : ↥S), 1 ⊗ₜ[K] x ∈ N v) ∧ ∀ (w : ↥T), 1 ⊗ₜ[K] x ∈ M w

Vector weak approximation, neighbourhood form. Given local vectors at finitely many finite and real places and a neighbourhood of each, one global vector of a finite-dimensional space over a number field has its localization in every one of these neighbourhoods. The localized spaces carry their module topologies.