The real numbers inside an archimedean completion

Let w be an infinite place of a field K. The completion w.Completion is a copy of ℝ when w is real and of ℂ when w is complex, and in either case it contains a canonical copy of ℝ: the real numbers are the elements sent into ℝ ⊆ ℂ by the extension embedding w.Completion → ℂ. At a complex place this does not depend on the embedding chosen to represent w, since the two conjugate embeddings agree on ℝ.

This file defines the resulting ring homomorphism Completion.ofReal w : ℝ →+* w.Completion. It is characterized by Completion.extensionEmbedding_ofReal, it is an isometry onto its image, and its normalized absolute value is |r| ^ w.mult. It supplies the positive real scalars at an infinite place, for instance an idele at one infinite place with any prescribed idele norm: the unit completionNormSection w t = t ^ (1 / m_w) has normalized absolute value t.

Main definitions

• NumberField.InfinitePlace.Completion.ofReal: the embedding ℝ →+* w.Completion.
• NumberField.InfinitePlace.completionNormSection: the positive real number t ^ (1 / m_w) as a unit of the completion K_w, a continuous homomorphism ℝ>0 →ₜ* K_wˣ.

Main results

• NumberField.InfinitePlace.Completion.extensionEmbedding_ofReal: the extension embedding sends ofReal w r to r; NumberField.InfinitePlace.Completion.eq_ofReal_iff says that this determines ofReal w r.
• NumberField.InfinitePlace.Completion.norm_ofReal and NumberField.InfinitePlace.Completion.isometry_ofReal: the embedding preserves absolute values.
• NumberField.InfinitePlace.completionNormalizedAbsValue_ofReal: the normalized absolute value of ofReal w r is |r| ^ w.mult.
• NumberField.InfinitePlace.exists_completionNormalizedAbsValue_eq: every nonnegative real number is a normalized absolute value.
• NumberField.InfinitePlace.completionNormalizedAbsValue_completionNormSection: the normalized absolute value of completionNormSection w t is t.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §4.

noncomputable def NumberField.InfinitePlace.Completion.ofReal {K : Type u_1} [Field K] (w : InfinitePlace K) : ℝ →+* w.Completion

The real numbers inside the completion at an infinite place w: the inverse of w.Completion ≃+* ℝ at a real place, and the inverse of w.Completion ≃+* ℂ restricted to ℝ at a complex place. It is characterized by extensionEmbedding_ofReal.

@[simp]

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_ofReal {K : Type u_1} [Field K] (w : InfinitePlace K) (r : ℝ) : (extensionEmbedding w) ((ofReal w) r) = ↑r

Characterization of ofReal: the extension embedding w.Completion → ℂ sends ofReal w r to the real number r.

theorem NumberField.InfinitePlace.Completion.eq_ofReal_iff {K : Type u_1} [Field K] (w : InfinitePlace K) {x : w.Completion} {r : ℝ} : x = (ofReal w) r ↔ (extensionEmbedding w) x = ↑r

An element of the completion is ofReal w r exactly when the extension embedding sends it to r.

@[simp]

theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_ofReal {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (r : ℝ) : (extensionEmbeddingOfIsReal hw) ((ofReal w) r) = r

At a real place, the real extension embedding sends ofReal w r to r.

@[simp]

theorem NumberField.InfinitePlace.Completion.norm_ofReal {K : Type u_1} [Field K] (w : InfinitePlace K) (r : ℝ) : ‖(ofReal w) r‖ = |r|

The embedding of ℝ into an archimedean completion preserves absolute values.

theorem NumberField.InfinitePlace.Completion.isometry_ofReal {K : Type u_1} [Field K] (w : InfinitePlace K) : Isometry ⇑(ofReal w)

The embedding of ℝ into an archimedean completion is an isometry.

theorem NumberField.InfinitePlace.Completion.continuous_ofReal {K : Type u_1} [Field K] (w : InfinitePlace K) : Continuous ⇑(ofReal w)

The embedding of ℝ into an archimedean completion is continuous.

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_ofReal {K : Type u_1} [Field K] (w : InfinitePlace K) (r : ℝ) : w.completionNormalizedAbsValue ((Completion.ofReal w) r) = |r| ^ w.mult

The normalized absolute value of a real number in the completion at w is its absolute value raised to the multiplicity of w.

theorem NumberField.InfinitePlace.exists_completionNormalizedAbsValue_eq {K : Type u_1} [Field K] (w : InfinitePlace K) {t : ℝ} (ht : 0 ≤ t) : ∃ (x : w.Completion), w.completionNormalizedAbsValue x = t

Every nonnegative real number is the normalized absolute value of an element of the completion at an infinite place, namely of the real number t ^ (1 / m_w).

The positive real units of norm t

noncomputable def NumberField.InfinitePlace.completionNormSection {K : Type u_1} [Field K] (w : InfinitePlace K) : NNRealˣ →ₜ* w.Completionˣ

The positive real number t ^ (1 / m_w) as a unit of the completion at the infinite place w, where m_w is the multiplicity of w. Its normalized absolute value is t (completionNormalizedAbsValue_completionNormSection).

@[simp]

theorem NumberField.InfinitePlace.coe_completionNormSection {K : Type u_1} [Field K] (w : InfinitePlace K) (t : NNRealˣ) : ↑(w.completionNormSection t) = (Completion.ofReal w) ↑(↑t ^ (↑w.mult)⁻¹)

The underlying element of completionNormSection w t is the real number t ^ (1 / m_w).

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_completionNormSection {K : Type u_1} [Field K] (w : InfinitePlace K) (t : NNRealˣ) : w.completionNormalizedAbsValue ↑(w.completionNormSection t) = ↑↑t

The normalized absolute value of completionNormSection w t is t.