Prescribing the signs of a number field element at the real places

Weak approximation says that a number field K is dense in the product of its completions at the infinite places; Mathlib records the diagonal form of this, NumberField.InfinitePlace.denseRange_algebraMap_pi, on the product of the copies of K carrying the topology of each infinite place. This file turns that topological statement into the arithmetic one it is used for: an element of K may be prescribed, independently at each real place, to be positive or negative there.

The passage is the usual one. Approximating the tuple whose entry at a place is 1 or -1 to within 1 forces the sign of each real embedding of the approximating element, because a real number within distance 1 of ±1 has the sign of ±1; the same estimate at any one place, real or complex, keeps the element away from 0.

Main results

• NumberField.exists_forall_infinitePlace_sub_lt: weak approximation at the infinite places in ε-δ form, with targets in K measured by the places themselves.
• NumberField.exists_forall_apply_eq_one_and_embedding_of_isReal_eq: the family of targets that such an approximation is aimed at, of absolute value one at every infinite place and of prescribed sign at every real place.
• NumberField.mul_pos_of_infinitePlace_sub_lt: an element within 1 of a target of absolute value one at a real place has the sign of that target there.
• NumberField.ne_zero_of_infinitePlace_sub_lt: an element within 1 of a target of absolute value one at any infinite place is nonzero.
• NumberField.exists_ne_zero_forall_isReal_pos: a nonzero element of K whose real embeddings have prescribed signs.
• NumberField.exists_ne_zero_neg_iff_mem: the same statement with the prescription given as the set of real places at which the element is to be negative.

References

The weak approximation theorem for pairwise inequivalent absolute values is Artin--Whaples; see E. Artin and G. Whaples, Axiomatic characterization of fields by the product formula for valuations, Bull. Amer. Math. Soc. 51 (1945), and, for the number field statement, J. W. S. Cassels and A. Fröhlich, Algebraic Number Theory, Chapter II.

theorem NumberField.exists_forall_infinitePlace_sub_lt {K : Type u_1} [Field K] [NumberField K] (a : InfinitePlace K → K) (r : InfinitePlace K → ℝ) (hr : ∀ (v : InfinitePlace K), 0 < r v) : ∃ (x : K), ∀ (v : InfinitePlace K), v (x - a v) < r v

Weak approximation at the infinite places. Given one target a v : K and one positive tolerance r v for each infinite place v of a number field, some single x : K is within r v of every target, as measured by the place at which that target was prescribed.

This is NumberField.InfinitePlace.denseRange_algebraMap_pi with the topology of the finite product unwound into the individual places.

theorem NumberField.exists_forall_apply_eq_one_and_embedding_of_isReal_eq {K : Type u_1} [Field K] (s : { w : InfinitePlace K // w.IsReal } → ℤˣ) : ∃ (b : InfinitePlace K → K), (∀ (v : InfinitePlace K), v (b v) = 1) ∧ ∀ (w : { w : InfinitePlace K // w.IsReal }), (InfinitePlace.embedding_of_isReal ⋯) (b ↑w) = ↑↑(s w)

A family of targets of absolute value one with prescribed signs. For any prescribed sign at each real place of a number field there is a family b, one element of K for each infinite place, whose entry at v has absolute value one at v and whose entry at a real place w has there exactly the prescribed sign.

This is the family that weak approximation at the infinite places is aimed at: absolute value one keeps an approximation of it away from 0, and NumberField.mul_pos_of_infinitePlace_sub_lt turns the approximation into a sign prescription.

theorem NumberField.mul_pos_of_infinitePlace_sub_lt {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) {x y : K} (hy : w y = 1) (h : w (x - y) < 1) : 0 < (InfinitePlace.embedding_of_isReal hw) y * (InfinitePlace.embedding_of_isReal hw) x

An approximation of a target of absolute value one has the sign of that target. At a real place w, an element x within 1 of a target y with w y = 1 has the same sign as y under the real embedding at w.

Together with NumberField.exists_forall_apply_eq_one_and_embedding_of_isReal_eq this is the whole archimedean content of a sign prescription: everything else is the approximation itself.

theorem NumberField.ne_zero_of_infinitePlace_sub_lt {K : Type u_1} [Field K] {w : InfinitePlace K} {x y : K} (hy : w y = 1) (h : w (x - y) < 1) : x ≠ 0

An element within 1 of a target of absolute value one at an infinite place is nonzero.

theorem NumberField.exists_ne_zero_forall_isReal_pos {K : Type u_1} [Field K] [NumberField K] (s : { w : InfinitePlace K // w.IsReal } → ℝ) (hs : ∀ (w : { w : InfinitePlace K // w.IsReal }), s w ≠ 0) : ∃ (x : K), x ≠ 0 ∧ ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < s w * (InfinitePlace.embedding_of_isReal ⋯) x

A nonzero element with prescribed signs at the real places. For any family of nonzero reals s, indexed by the real infinite places of a number field K, some nonzero x : K has s w and the image of x under the real embedding at w of the same sign, at every real place w simultaneously.

theorem NumberField.exists_ne_zero_neg_iff_mem {K : Type u_1} [Field K] [NumberField K] (S : Set { w : InfinitePlace K // w.IsReal }) : ∃ (x : K), x ≠ 0 ∧ ∀ (w : { w : InfinitePlace K // w.IsReal }), (InfinitePlace.embedding_of_isReal ⋯) x < 0 ↔ w ∈ S

A nonzero element of K negative at exactly a prescribed set of real places. Since the real places at which an element is negative determine its sign pattern, this is NumberField.exists_ne_zero_forall_isReal_pos with the pattern presented as a set.