Normalized absolute values on archimedean completions

NumberField.InfinitePlace.completionNormalizedAbsValue is the norm on w.Completion raised to w.mult, as a multiplicative map with zero. The exponent is one at real places and two at complex places. For a number field, its restriction agrees with the normalization in NumberField.prod_abs_eq_one; these completion-side maps supply the archimedean factors of the idele norm.

NumberField.InfinitePlace.Completion.norm_algebraMap compares the completion norm with the place absolute value on the dense base field. The normalized value is continuous and takes every nonnegative real value.

Archimedean completions are nontrivially normed fields, and the diagonal embeddings form scalar towers over any commutative semiring base.

References

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

@[instance_reducible]

noncomputable instance NumberField.InfinitePlace.Completion.instNontriviallyNormedField {K : Type u_1} [Field K] (v : InfinitePlace K) : NontriviallyNormedField v.Completion

An archimedean completion is a nontrivially normed field.

Equations

• NumberField.InfinitePlace.Completion.instNontriviallyNormedField v = { toNormedField := NumberField.InfinitePlace.Completion.instNormedField v, non_trivial := ⋯ }

instance NumberField.InfinitePlace.instIsScalarTowerCompletion_tauCeti {K : Type u_1} [Field K] {R : Type u_2} [CommSemiring R] [Algebra R K] (w : InfinitePlace K) : IsScalarTower R K w.Completion

The diagonal algebra structures on an archimedean completion form a scalar tower.

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

The normalized absolute value on the completion at an infinite place.

Equations

• w.completionNormalizedAbsValue = (powMonoidWithZeroHom ⋯).comp normHom

@[simp]

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_apply {K : Type u_1} [Field K] (w : InfinitePlace K) (x : w.Completion) : w.completionNormalizedAbsValue x = ‖x‖ ^ w.mult

Evaluating the normalized absolute value at x gives ‖x‖ ^ w.mult.

@[simp]

theorem NumberField.InfinitePlace.Completion.norm_algebraMap {K : Type u_1} [Field K] (w : InfinitePlace K) (x : K) : ‖(algebraMap K w.Completion) x‖ = w x

The norm of a field element in its archimedean completion is its place absolute value.

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_algebraMap {K : Type u_1} [Field K] (w : InfinitePlace K) (x : K) : w.completionNormalizedAbsValue ((algebraMap K w.Completion) x) = w x ^ w.mult

On the dense copy of K, the infinite completion value is the normalized infinite-place value.

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_algebraMap_of_isReal {K : Type u_1} [Field K] (w : InfinitePlace K) (hw : w.IsReal) (x : K) : w.completionNormalizedAbsValue ((algebraMap K w.Completion) x) = w x

On the dense copy of K, a real place contributes its ordinary absolute value.

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_algebraMap_of_isComplex {K : Type u_1} [Field K] (w : InfinitePlace K) (hw : w.IsComplex) (x : K) : w.completionNormalizedAbsValue ((algebraMap K w.Completion) x) = w x ^ 2

On the dense copy of K, a complex place contributes the square of its absolute value.

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_of_isReal {K : Type u_1} [Field K] (w : InfinitePlace K) (hw : w.IsReal) (x : w.Completion) : w.completionNormalizedAbsValue x = ‖x‖

At a real place the completion value is the ordinary absolute value.

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_of_isComplex {K : Type u_1} [Field K] (w : InfinitePlace K) (hw : w.IsComplex) (x : w.Completion) : w.completionNormalizedAbsValue x = ‖x‖ ^ 2

At a complex place the completion value is the square of the ordinary absolute value.

theorem NumberField.InfinitePlace.continuous_completionNormalizedAbsValue {K : Type u_1} [Field K] (w : InfinitePlace K) : Continuous ⇑w.completionNormalizedAbsValue

The infinite completion value is continuous.

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.