Finite places of number fields

This file records general facts about the finite places of a number field.

The nonzero values of a finite place are exactly the integer powers of its prime norm (apply_eq_absNorm_zpow, exists_ne_zero_apply_eq_absNorm_zpow), using Mathlib's HeightOneSpectrum.valuation_surjective for attainment.

The valuation dictionary FinitePlace.mk_apply_le_one_iff and FinitePlace.mk_apply_eq_one_iff compares the finite-place absolute value with the adic valuation. These comparisons follow Ralf Stephan's ArithmeticHeights/SUnit.lean in rwst/Subspace-Theorems at e443c2479e19f7665b31d8e94e2317c8ced1ca06 (Apache 2.0). FinitePlace.mk_apply_le_one_iff_algebraMap_mem reads integrality in the adic completion instead.

The file also records that a number field always has a finite place: the finite places are the height one primes of its ring of integers, and that ring is a Dedekind domain which is not a field, so it has a maximal ideal. Recording this as a Nonempty instance lets local-global arguments pick a finite place with Classical.arbitrary whenever a hypothesis quantified over all finite places has to be used at some place — for instance to read off an invariant, such as the dimension of the underlying space, that is the same at every place. Without the instance each such argument has to rebuild the existence proof inline.

Two finite places are equal exactly when their absolute values are equivalent, NumberField.FinitePlace.eq_iff_isEquiv, as Mathlib has for infinite places. For a prime w of a finite extension over a prime v, Mathlib's equivHeightOneSpectrum_symm_apply_algebraMap shows that on the base, the finite place of w is the e * f-th power of that of v.

NumberField.HeightOneSpectrum.log_adicAbv reads the logarithm of the v-adic absolute value as minus the v-adic order times log N(v), the form in which valuations enter height estimates.

NumberField.FinitePlace.finprod_comp_mk reindexes a product over the finite places by the height one primes of the ring of integers.

Finally, NumberField.FinitePlace.hasFiniteMulSupport_iSup records that the maximum of the finite-place absolute values of the coordinates of a nonzero finite tuple is 1 at all but finitely many finite places, and NumberField.FinitePlace.hasFiniteMulSupport_max_one and NumberField.FinitePlace.hasFiniteMulSupport_min_one record the same for the absolute value of an element truncated from below or above at 1.

An algebraic integer is at most 1 at every finite place, NumberField.FinitePlace.apply_le_one, and NumberField.FinitePlace.exists_ne_zero_forall_apply_le produces a nonzero algebraic integer which is as small as prescribed at finitely many finite places. Its form NumberField.FinitePlace.exists_ne_zero_forall_mul_apply_le clears prescribed bounds R v at those places: v d * R v ≤ 1. When a finite place u lies outside that finite set, NumberField.FinitePlace.exists_apply_eq_one_forall_apply_le and NumberField.FinitePlace.exists_apply_eq_one_forall_mul_apply_le choose d to have u d = 1 as well. These follow Ralf Stephan's DiophantineApproximation/FinitePlaceValues.lean in rwst/Subspace-Theorems, snapshot c26d909dc48cf7fe (Apache 2.0).

instance TauCeti.instNonemptyHeightOneSpectrumRingOfIntegersOfNumberField_tauCeti {K : Type u_1} [Field K] [NumberField K] : Nonempty (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

A number field has a finite place: its ring of integers is not a field.

theorem NumberField.FinitePlace.apply_eq_absNorm_zpow {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) {x : K} (hx : x ≠ 0) : v x = ↑(Ideal.absNorm v.maximalIdeal.asIdeal) ^ ((IsDedekindDomain.HeightOneSpectrum.valuation K v.maximalIdeal) x).log

Every nonzero finite-place value is an integer power of the norm of its prime.

theorem NumberField.FinitePlace.norm_adicCompletion_eq_absNorm_zpow {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (hx : x ≠ 0) : ‖x‖ = ↑(Ideal.absNorm v.asIdeal) ^ (Valued.v x).log

The norm of a nonzero element of the v-adic completion is the norm of v raised to the logarithm of its valuation. In particular a uniformizer, of valuation exp (-1), has norm N(v)⁻¹.

theorem NumberField.FinitePlace.exists_ne_zero_apply_eq_absNorm_zpow {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) (n : ℤ) : ∃ (x : K), x ≠ 0 ∧ v x = ↑(Ideal.absNorm v.maximalIdeal.asIdeal) ^ n

Every integer power of the prime norm occurs as a nonzero finite-place value.

theorem NumberField.FinitePlace.mk_apply_le_one_iff {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : (mk v) x ≤ 1 ↔ (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≤ 1

An element is integral at a prime iff its finite-place absolute value is at most one.

theorem NumberField.FinitePlace.mk_apply_le_one_iff_algebraMap_mem {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : (mk v) x ≤ 1 ↔ (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

An element is integral at a prime iff its finite-place absolute value is at most one, read in the completion: its image lies in the ring of integers of the adic completion.

theorem NumberField.FinitePlace.mk_apply_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : (mk v) x = 1 ↔ (IsDedekindDomain.HeightOneSpectrum.valuation K v) x = 1

An element has valuation one at a prime iff its finite-place absolute value is one.

theorem NumberField.FinitePlace.eq_iff_isEquiv {K : Type u_1} [Field K] [NumberField K] {w v : FinitePlace K} : w = v ↔ (↑w).IsEquiv ↑v

Two finite places of a number field are equal if and only if their absolute values are equivalent. This is the finite counterpart of Mathlib's InfinitePlace.eq_iff_isEquiv.

theorem NumberField.FinitePlace.finprod_comp_mk {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [CommMonoid M] (f : FinitePlace K → M) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), f (mk v) = ∏ᶠ (w : FinitePlace K), f w

A product over the finite places of a number field, reindexed by the height one primes of its ring of integers.

theorem NumberField.FinitePlace.hasFiniteMulSupport_iSup {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {y : ι → K} (hy : y ≠ 0) : Function.HasFiniteMulSupport fun (v : FinitePlace K) => ⨆ (i : ι), v (y i)

For a nonzero tuple over a number field, the maximum of the finite-place absolute values of its coordinates is 1 at all but finitely many finite places.

theorem NumberField.FinitePlace.hasFiniteMulSupport_max_one {K : Type u_1} [Field K] [NumberField K] (x : K) : Function.HasFiniteMulSupport fun (v : FinitePlace K) => max (v x) 1

Truncating the finite places of x from below keeps finite multiplicative support. For x = 0 the family is constantly 1.

theorem NumberField.FinitePlace.hasFiniteMulSupport_min_one {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : Function.HasFiniteMulSupport fun (v : FinitePlace K) => min 1 (v x)

Truncating the finite places of a nonzero x from above keeps finite multiplicative support.

theorem NumberField.FinitePlace.apply_le_one {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) (x : RingOfIntegers K) : v ↑x ≤ 1

An algebraic integer has absolute value at most 1 at every finite place.

theorem NumberField.FinitePlace.exists_ne_zero_forall_apply_le {K : Type u_1} [Field K] [NumberField K] (T : Finset (FinitePlace K)) {ε : FinitePlace K → ℝ} (hε : ∀ v ∈ T, 0 < ε v) : ∃ (d : RingOfIntegers K), d ≠ 0 ∧ ∀ v ∈ T, v ↑d ≤ ε v

Some nonzero algebraic integer is as small as prescribed at every place of a finite set of finite places.

theorem NumberField.FinitePlace.exists_ne_zero_forall_mul_apply_le {K : Type u_1} [Field K] [NumberField K] (T : Finset (FinitePlace K)) {R : FinitePlace K → ℝ} (hR : ∀ v ∈ T, 0 ≤ R v) : ∃ (d : RingOfIntegers K), d ≠ 0 ∧ ∀ v ∈ T, v ↑d * R v ≤ 1

Some nonzero algebraic integer clears prescribed nonnegative bounds at every place of a finite set of finite places: v d * R v ≤ 1 there.

theorem NumberField.FinitePlace.exists_apply_eq_one_forall_apply_le {K : Type u_1} [Field K] [NumberField K] (u : FinitePlace K) {T : Finset (FinitePlace K)} (hu : u ∉ T) {ε : FinitePlace K → ℝ} (hε : ∀ v ∈ T, 0 < ε v) : ∃ (d : RingOfIntegers K), u ↑d = 1 ∧ ∀ v ∈ T, v ↑d ≤ ε v

Given a finite place u outside a finite set T of finite places, some algebraic integer has absolute value 1 at u and is as small as prescribed at every place of T.

theorem NumberField.FinitePlace.exists_apply_eq_one_forall_mul_apply_le {K : Type u_1} [Field K] [NumberField K] (u : FinitePlace K) {T : Finset (FinitePlace K)} (hu : u ∉ T) {R : FinitePlace K → ℝ} (hR : ∀ v ∈ T, 0 ≤ R v) : ∃ (d : RingOfIntegers K), u ↑d = 1 ∧ ∀ v ∈ T, v ↑d * R v ≤ 1

Given a finite place u outside a finite set T of finite places, some algebraic integer has absolute value 1 at u and clears prescribed nonnegative bounds R v at every place of T: v d * R v ≤ 1 there.

theorem NumberField.HeightOneSpectrum.log_adicAbv {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : Real.log ((adicAbv K v) x) = ↑((IsDedekindDomain.HeightOneSpectrum.valuation K v) x).log * Real.log ↑(Ideal.absNorm v.asIdeal)

The logarithm of the v-adic absolute value of x is -ord_v(x) times the logarithm of the norm of v, where ord_v(x) = -WithZero.log (v.valuation K x) is the v-adic order of x. Both sides vanish at x = 0.