Finite places of number fields #

This file defines finite places of a number field K as absolute values coming from an embedding into a completion of K associated to a non-zero prime ideal of 𝓞 K.

Main Definitions and Results #

NumberField.adicAbv: a v-adic absolute value on K.
NumberField.FinitePlace: the type of finite places of a number field K.
NumberField.FinitePlace.embedding: the canonical embedding of a number field K to the v-adic completion v.adicCompletion K of K, where v is a non-zero prime ideal of 𝓞 K
NumberField.FinitePlace.norm_def: the norm of embedding v x is the same as the v-adic absolute value of x. See also NumberField.FinitePlace.norm_def' and NumberField.FinitePlace.norm_def_int for versions where the v-adic absolute value is unfolded.
NumberField.FinitePlace.mulSupport_finite: the v-adic absolute value of a non-zero element of K is different from 1 for at most finitely many v.

Tags #

number field, places, finite places

source

theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

1 < Ideal.absNorm v.asIdeal

The norm of a maximal ideal is > 1

source

@[deprecated NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm (since := "2025-02-28")]

theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_norm {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

1 < Ideal.absNorm v.asIdeal

Alias of NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm.

The norm of a maximal ideal is > 1

source

theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

1 < ↑(Ideal.absNorm v.asIdeal)

The norm of a maximal ideal as an element of ℝ≥0 is > 1

source

@[deprecated NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal (since := "2025-02-28")]

theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_norm_nnreal {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

1 < ↑(Ideal.absNorm v.asIdeal)

Alias of NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal.

The norm of a maximal ideal as an element of ℝ≥0 is > 1

source

theorem NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

↑(Ideal.absNorm v.asIdeal) ≠ 0

The norm of a maximal ideal as an element of ℝ≥0 is ≠ 0

source

@[deprecated NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero (since := "2025-02-28")]

theorem NumberField.RingOfIntegers.HeightOneSpectrum.norm_ne_zero {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

↑(Ideal.absNorm v.asIdeal) ≠ 0

Alias of NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero.

The norm of a maximal ideal as an element of ℝ≥0 is ≠ 0

source

noncomputable def NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

AbsoluteValue K ℝ

The v-adic absolute value on K defined as the norm of v raised to negative v-adic valuation

Equations

Instances For

source

@[deprecated NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv (since := "2025-02-28")]

def NumberField.RingOfIntegers.HeightOneSpectrum.vadicAbv {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

AbsoluteValue K ℝ

Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv.

The v-adic absolute value on K defined as the norm of v raised to negative v-adic valuation

Equations

Instances For

source

theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {x : K} :

(adicAbv v) x = ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))

source

@[deprecated NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def (since := "2025-02-28")]

theorem NumberField.RingOfIntegers.HeightOneSpectrum.vadicAbv_def {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {x : K} :

(adicAbv v) x = ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))

Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def.

source

theorem NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

IsNonarchimedean ⇑(adicAbv v)

The v-adic absolute value is nonarchimedean

source

noncomputable def NumberField.FinitePlace.embedding {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v) →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

The embedding of a number field inside its completion with respect to v.

Equations

Instances For

source

@[deprecated NumberField.FinitePlace.embedding (since := "2025-02-28")]

def NumberField.embedding {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v) →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

Alias of NumberField.FinitePlace.embedding.

The embedding of a number field inside its completion with respect to v.

Equations

Instances For

source

theorem NumberField.FinitePlace.embedding_apply {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) :

(embedding v) x = ↑x

source

noncomputable instance NumberField.instRankOneValuedAdicCompletion {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

Valued.v.RankOne

Equations

source

noncomputable instance NumberField.instNormedFieldValuedAdicCompletion {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

NormedField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

The v-adic completion of K is a normed field.

Equations

source

def NumberField.FinitePlace (K : Type u_2) [Field K] [NumberField K] :

Type u_2

A finite place of a number field K is a place associated to an embedding into a completion with respect to a maximal ideal.

Equations

Instances For

source

noncomputable def NumberField.FinitePlace.mk {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

FinitePlace K

Return the finite place defined by a maximal ideal v.

Equations

Instances For

source

theorem NumberField.toNNReal_valued_eq_adicAbv {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)) :

↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x)) = (RingOfIntegers.HeightOneSpectrum.adicAbv v) x

source

@[deprecated NumberField.toNNReal_valued_eq_adicAbv (since := "2025-03-01")]

theorem NumberField.toNNReal_Valued_eq_vadicAbv {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)) :

↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x)) = (RingOfIntegers.HeightOneSpectrum.adicAbv v) x

Alias of NumberField.toNNReal_valued_eq_adicAbv.

source

theorem NumberField.FinitePlace.norm_def {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)) :

‖(embedding v) x‖ = (RingOfIntegers.HeightOneSpectrum.adicAbv v) x

The norm of the image after the embedding associated to v is equal to the v-adic absolute value.

source

theorem NumberField.FinitePlace.norm_def' {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)) :

‖(embedding v) x‖ = ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))

The norm of the image after the embedding associated to v is equal to the norm of v raised to the power of the v-adic valuation.

source

theorem NumberField.FinitePlace.norm_def_int {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))) :

‖(embedding v) ↑x‖ = ↑((WithZeroMulInt.toNNReal ⋯) (v.intValuation x))

The norm of the image after the embedding associated to v is equal to the norm of v raised to the power of the v-adic valuation for integers.

source

theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x y : K) :

(adicAbv v) (x + y) ≤ max ((adicAbv v) x) ((adicAbv v) y)

The v-adic absolute value satisfies the ultrametric inequality.

source

@[deprecated NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max (since := "2025-02-28")]

theorem NumberField.vadicAbv_add_le_max {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x y : K) :

(RingOfIntegers.HeightOneSpectrum.adicAbv v) (x + y) ≤ max ((RingOfIntegers.HeightOneSpectrum.adicAbv v) x) ((RingOfIntegers.HeightOneSpectrum.adicAbv v) y)

Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max.

The v-adic absolute value satisfies the ultrametric inequality.

source

theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (n : ℕ) :

(adicAbv v) ↑n ≤ 1

The v-adic absolute value of a natural number is ≤ 1.

source

@[deprecated NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one (since := "2025-02-28")]

theorem NumberField.vadicAbv_natCast_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (n : ℕ) :

(RingOfIntegers.HeightOneSpectrum.adicAbv v) ↑n ≤ 1

Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one.

The v-adic absolute value of a natural number is ≤ 1.

source

theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (n : ℤ) :

(adicAbv v) ↑n ≤ 1

The v-adic absolute value of an integer is ≤ 1.

source

@[deprecated NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one (since := "2025-02-28")]

theorem NumberField.vadicAbv_intCast_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (n : ℤ) :

(RingOfIntegers.HeightOneSpectrum.adicAbv v) ↑n ≤ 1

Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one.

The v-adic absolute value of an integer is ≤ 1.

source

theorem NumberField.FinitePlace.norm_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))) :

‖(embedding v) ↑x‖ ≤ 1

The v-adic norm of an integer is at most 1.

source

@[deprecated NumberField.FinitePlace.norm_le_one (since := "2025-02-28")]

theorem NumberField.norm_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))) :

‖(FinitePlace.embedding v) ↑x‖ ≤ 1

Alias of NumberField.FinitePlace.norm_le_one.

The v-adic norm of an integer is at most 1.

source

theorem NumberField.FinitePlace.norm_eq_one_iff_notMem {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))) :

‖(embedding v) ↑x‖ = 1 ↔ x ∉ v.asIdeal

The v-adic norm of an integer is 1 if and only if it is not in the ideal.

source

@[deprecated NumberField.FinitePlace.norm_eq_one_iff_notMem (since := "2025-05-23")]

theorem NumberField.FinitePlace.norm_eq_one_iff_not_mem {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))) :

‖(embedding v) ↑x‖ = 1 ↔ x ∉ v.asIdeal

Alias of NumberField.FinitePlace.norm_eq_one_iff_notMem.

The v-adic norm of an integer is 1 if and only if it is not in the ideal.

source

@[deprecated NumberField.FinitePlace.norm_eq_one_iff_not_mem (since := "2025-02-28")]

theorem NumberField.norm_eq_one_iff_not_mem {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))) :

‖(FinitePlace.embedding v) ↑x‖ = 1 ↔ x ∉ v.asIdeal

Alias of NumberField.FinitePlace.norm_eq_one_iff_notMem.

The v-adic norm of an integer is 1 if and only if it is not in the ideal.

source

theorem NumberField.FinitePlace.norm_lt_one_iff_mem {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))) :

‖(embedding v) ↑x‖ < 1 ↔ x ∈ v.asIdeal

The v-adic norm of an integer is less than 1 if and only if it is in the ideal.

source

@[deprecated NumberField.FinitePlace.norm_lt_one_iff_mem (since := "2025-02-28")]

theorem NumberField.norm_lt_one_iff_mem {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))) :

‖(FinitePlace.embedding v) ↑x‖ < 1 ↔ x ∈ v.asIdeal

Alias of NumberField.FinitePlace.norm_lt_one_iff_mem.

The v-adic norm of an integer is less than 1 if and only if it is in the ideal.

source

instance NumberField.FinitePlace.instFunLikeReal {K : Type u_1} [Field K] [NumberField K] :

FunLike (FinitePlace K) K ℝ

Equations

source

instance NumberField.FinitePlace.instMonoidWithZeroHomClassReal {K : Type u_1} [Field K] [NumberField K] :

MonoidWithZeroHomClass (FinitePlace K) K ℝ

source

instance NumberField.FinitePlace.instNonnegHomClassReal {K : Type u_1} [Field K] [NumberField K] :

NonnegHomClass (FinitePlace K) K ℝ

source

@[simp]

theorem NumberField.FinitePlace.mk_apply {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) :

(mk v) x = ‖(embedding v) x‖

source

@[deprecated NumberField.FinitePlace.mk_apply (since := "2025-02-28")]

theorem NumberField.FinitePlace.apply {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) :

(mk v) x = ‖(embedding v) x‖

Alias of NumberField.FinitePlace.mk_apply.

source

noncomputable def NumberField.FinitePlace.maximalIdeal {K : Type u_1} [Field K] [NumberField K] (w : FinitePlace K) :

IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)

For a finite place w, return a maximal ideal v such that w = finite_place v .

Equations

Instances For

source

@[simp]

theorem NumberField.FinitePlace.mk_maximalIdeal {K : Type u_1} [Field K] [NumberField K] (w : FinitePlace K) :

mk w.maximalIdeal = w

source

@[simp]

theorem NumberField.FinitePlace.norm_embedding_eq {K : Type u_1} [Field K] [NumberField K] (w : FinitePlace K) (x : K) :

‖(embedding w.maximalIdeal) x‖ = w x

source

theorem NumberField.FinitePlace.pos_iff {K : Type u_1} [Field K] [NumberField K] {w : FinitePlace K} {x : K} :

0 < w x ↔ x ≠ 0

source

@[simp]

theorem NumberField.FinitePlace.mk_eq_iff {K : Type u_1} [Field K] [NumberField K] {v₁ v₂ : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} :

mk v₁ = mk v₂ ↔ v₁ = v₂

source

theorem NumberField.FinitePlace.maximalIdeal_mk {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

(mk v).maximalIdeal = v

source

noncomputable def NumberField.FinitePlace.equivHeightOneSpectrum {K : Type u_1} [Field K] [NumberField K] :

FinitePlace K ≃ IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)

The equivalence between finite places and maximal ideals.

Equations

Instances For

source

theorem NumberField.FinitePlace.maximalIdeal_injective {K : Type u_1} [Field K] [NumberField K] :

Function.Injective fun (w : FinitePlace K) => w.maximalIdeal

source

theorem NumberField.FinitePlace.maximalIdeal_inj {K : Type u_1} [Field K] [NumberField K] (w₁ w₂ : FinitePlace K) :

w₁.maximalIdeal = w₂.maximalIdeal ↔ w₁ = w₂

source

theorem NumberField.FinitePlace.mulSupport_finite_int {K : Type u_1} [Field K] [NumberField K] {x : RingOfIntegers K} (h_x_nezero : x ≠ 0) :

(Function.mulSupport fun (w : FinitePlace K) => w ↑x).Finite

source

theorem NumberField.FinitePlace.mulSupport_finite {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) :

(Function.mulSupport fun (w : FinitePlace K) => w x).Finite

source

theorem IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K) :

(NumberField.FinitePlace.equivHeightOneSpectrum.symm v) x = ‖(NumberField.FinitePlace.embedding v) x‖

source

theorem IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {x : NumberField.RingOfIntegers (WithVal (valuation K v))} (h_x_nezero : x ≠ 0) :

‖(NumberField.FinitePlace.embedding v) ↑x‖ * ↑(Ideal.absNorm (v.maxPowDividing (Ideal.span {x}))) = 1

Documentation

Mathlib.NumberTheory.NumberField.FinitePlaces

Finite places of number fields #

Main Definitions and Results #

Tags #