Documentation

Mathlib.NumberTheory.NumberField.FinitePlaces

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.
The valuation subrings of the field at the v-valuation and it's adic completion are discrete valuation rings.

Tags #

number field, places, finite places

instance instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A) :

IsPrincipalIdealRing ↥(IsDedekindDomain.HeightOneSpectrum.valuation K v).integer

instance instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A) :

IsDiscreteValuationRing ↥(IsDedekindDomain.HeightOneSpectrum.valuation K v).integer

instance instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A) :

IsPrincipalIdealRing ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

instance instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A) :

IsDiscreteValuationRing ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

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

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

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

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

NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv v = v.adicAbv ⋯

Instances For

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))

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

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

NumberField.FinitePlace.embedding v = UniformSpace.Completion.coeRingHom

Instances For

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

(embedding v) x = ↑x

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

(IsDedekindDomain.HeightOneSpectrum.valuation K v).RankOne

Equations

One or more equations did not get rendered due to their size.

@[deprecated Valuation.instRankOneCompletion (since := "2026-01-05")]

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

Valued.v.RankOne

Equations

NumberField.instRankOneValuedAdicCompletion v = inferInstance

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

NumberField.instNormedFieldValuedAdicCompletion v = Valued.toNormedField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (WithZero (Multiplicative ℤ))

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

One or more equations did not get rendered due to their size.

Instances For

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

Return the finite place defined by a maximal ideal v.

Equations

NumberField.FinitePlace.mk v = ⟨NumberField.place (NumberField.FinitePlace.embedding v), ⋯⟩

Instances For

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

def NumberField.IsFinitePlace {K : Type u_1} [Field K] [NumberField K] (w : AbsoluteValue K ℝ) :

A predicate singling out finite places among the absolute values on a number field K.

Equations

NumberField.IsFinitePlace w = ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), NumberField.place (NumberField.FinitePlace.embedding v) = w

Instances For

theorem NumberField.FinitePlace.isFinitePlace {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) :

IsFinitePlace ↑v

theorem NumberField.isFinitePlace_iff {K : Type u_1} [Field K] [NumberField K] (v : AbsoluteValue K ℝ) :

IsFinitePlace v ↔ ∃ (w : FinitePlace K), ↑w = v

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

FunLike (FinitePlace K) K ℝ

Equations

NumberField.FinitePlace.instFunLikeReal = { coe := fun (w : NumberField.FinitePlace K) (x : K) => ↑w x, coe_injective' := ⋯ }

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

MonoidWithZeroHomClass (FinitePlace K) K ℝ

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

NonnegHomClass (FinitePlace K) K ℝ

@[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‖

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

v x = ↑v x

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

w.maximalIdeal = ⋯.choose

Instances For

@[simp]

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

mk w.maximalIdeal = w

@[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

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

0 < w x ↔ x ≠ 0

@[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₂

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

(mk v).maximalIdeal = v

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

NumberField.FinitePlace.equivHeightOneSpectrum = { toFun := NumberField.FinitePlace.maximalIdeal, invFun := NumberField.FinitePlace.mk, left_inv := ⋯, right_inv := ⋯ }

Instances For

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

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

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

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

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

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

theorem NumberField.FinitePlace.add_le {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) (x y : K) :

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

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

NonarchimedeanHomClass (FinitePlace K) K ℝ

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‖

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