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 ⋯

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

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.instRankOneValuedAdicCompletion {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : Valued.v.RankOne

Equations

• NumberField.instRankOneValuedAdicCompletion v = { toIsNontrivial := ⋯, hom := { toFun := ⇑(WithZeroMulInt.toNNReal ⋯), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }, strictMono' := ⋯ }

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.

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

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

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

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

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.

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

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‖

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

@[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 := ⋯ }

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