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.

Many of the results in this file are expressed in the generality of: R is a Dedekind domain with field of fractions K such that Module.Finite ℤ R and Module.Free ℤ R. If K is a number field, then this characterises R as being isomorphic to 𝓞 K without explicitly requiring 𝓞 K. This is so that ℤ and 𝓞 ℚ can be used interchangeably.

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_embedding: the norm of embedding v x is the same as the v-adic absolute value of x. See also NumberField.FinitePlace.norm_embedding' and NumberField.FinitePlace.norm_embedding_int for versions where the v-adic absolute value is unfolded.
• NumberField.FinitePlace.hasFiniteMulSupport: 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)

noncomputable def NumberField.FinitePlace.embedding {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : K →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

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

theorem NumberField.FinitePlace.embedding_apply {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : K) : (embedding v) x = ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm x)

instance NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Valued.v.IsRankOneDiscrete

In this section we assume further that Module.Finite ℤ R and Module.Free ℤ R. This characterises R as being isomorphic to 𝓞 K without explicitly requiring that type. As a result, if F = ℚ, then we can use ℤ and 𝓞 ℚ interchangeably.

theorem NumberField.HeightOneSpectrum.one_lt_absNorm {R : Type u_2} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : 1 < Ideal.absNorm v.asIdeal

The norm of a maximal ideal is > 1

theorem NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal {R : Type u_2} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : 1 < ↑(Ideal.absNorm v.asIdeal)

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

theorem NumberField.HeightOneSpectrum.absNorm_ne_zero {R : Type u_2} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : ↑(Ideal.absNorm v.asIdeal) ≠ 0

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

noncomputable def NumberField.HeightOneSpectrum.adicAbv (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : AbsoluteValue K ℝ

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

theorem NumberField.HeightOneSpectrum.adicAbv_def (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] {x : K} : (adicAbv K v) x = ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))

theorem NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : IsNonarchimedean ⇑(adicAbv K v)

The v-adic absolute value is nonarchimedean

@[implicit_reducible]

noncomputable instance NumberField.HeightOneSpectrum.instRankOneWithZeroMultiplicativeIntValuation (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : (IsDedekindDomain.HeightOneSpectrum.valuation K v).RankOne

@[implicit_reducible]

noncomputable instance NumberField.HeightOneSpectrum.instRankOneAdicCompletion (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : Valued.v.RankOne

theorem NumberField.HeightOneSpectrum.rankOne_hom'_def (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : Valuation.RankLeOne.hom' Valued.v = (WithZeroMulInt.toNNReal ⋯).comp (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt Valued.v).toMonoidWithZeroHom

@[implicit_reducible]

noncomputable instance NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : NormedField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

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

theorem NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)) : ↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x)) = (adicAbv K v) ((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)) x)

theorem NumberField.HeightOneSpectrum.adicAbv_add_le_max (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x y : K) : (adicAbv K v) (x + y) ≤ max ((adicAbv K v) x) ((adicAbv K v) y)

The v-adic absolute value satisfies the ultrametric inequality.

theorem NumberField.HeightOneSpectrum.adicAbv_natCast_le_one (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (n : ℕ) : (adicAbv K v) ↑n ≤ 1

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

theorem NumberField.HeightOneSpectrum.adicAbv_intCast_le_one (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (n : ℤ) : (adicAbv K v) ↑n ≤ 1

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

@[deprecated NumberField.HeightOneSpectrum.one_lt_absNorm (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm {R : Type u_2} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : 1 < Ideal.absNorm v.asIdeal

Alias of NumberField.HeightOneSpectrum.one_lt_absNorm.

---

The norm of a maximal ideal is > 1

@[deprecated NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal {R : Type u_2} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : 1 < ↑(Ideal.absNorm v.asIdeal)

Alias of NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal.

---

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

@[deprecated NumberField.HeightOneSpectrum.absNorm_ne_zero (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero {R : Type u_2} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : ↑(Ideal.absNorm v.asIdeal) ≠ 0

Alias of NumberField.HeightOneSpectrum.absNorm_ne_zero.

---

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

@[deprecated NumberField.HeightOneSpectrum.adicAbv (since := "2026-03-11")]

def NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : AbsoluteValue K ℝ

Alias of NumberField.HeightOneSpectrum.adicAbv.

---

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

@[deprecated NumberField.HeightOneSpectrum.adicAbv_def (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] {x : K} : (NumberField.HeightOneSpectrum.adicAbv K v) x = ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))

Alias of NumberField.HeightOneSpectrum.adicAbv_def.

@[deprecated NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : IsNonarchimedean ⇑(NumberField.HeightOneSpectrum.adicAbv K v)

Alias of NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv.

---

The v-adic absolute value is nonarchimedean

@[deprecated NumberField.HeightOneSpectrum.instRankOneAdicCompletion (since := "2026-03-11")]

def NumberField.HeightOneSpectrum.NumberField.instRankOneAdicCompletion (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : Valued.v.RankOne

Alias of NumberField.HeightOneSpectrum.instRankOneAdicCompletion.

@[deprecated NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion (since := "2026-03-11")]

def NumberField.HeightOneSpectrum.NumberField.instNormedFieldValuedAdicCompletion (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : NormedField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

Alias of NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion.

---

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

@[deprecated NumberField.HeightOneSpectrum.rankOne_hom'_def (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : Valuation.RankLeOne.hom' Valued.v = (WithZeroMulInt.toNNReal ⋯).comp (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt Valued.v).toMonoidWithZeroHom

Alias of NumberField.HeightOneSpectrum.rankOne_hom'_def.

@[deprecated NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)) : ↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x)) = (adicAbv K v) ((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)) x)

Alias of NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv.

@[deprecated NumberField.HeightOneSpectrum.adicAbv_add_le_max (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x y : K) : (NumberField.HeightOneSpectrum.adicAbv K v) (x + y) ≤ max ((NumberField.HeightOneSpectrum.adicAbv K v) x) ((NumberField.HeightOneSpectrum.adicAbv K v) y)

Alias of NumberField.HeightOneSpectrum.adicAbv_add_le_max.

---

The v-adic absolute value satisfies the ultrametric inequality.

@[deprecated NumberField.HeightOneSpectrum.adicAbv_natCast_le_one (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (n : ℕ) : (NumberField.HeightOneSpectrum.adicAbv K v) ↑n ≤ 1

Alias of NumberField.HeightOneSpectrum.adicAbv_natCast_le_one.

---

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

@[deprecated NumberField.HeightOneSpectrum.adicAbv_intCast_le_one (since := "2026-03-11")]

theorem NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (n : ℤ) : (NumberField.HeightOneSpectrum.adicAbv K v) ↑n ≤ 1

Alias of NumberField.HeightOneSpectrum.adicAbv_intCast_le_one.

---

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

theorem NumberField.FinitePlace.norm_def {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) : ‖x‖ = ↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x))

The norm of an element in the v-adic completion of K. See FinitePlace.norm_embedding for the equality involving ‖embedding v x‖ on the LHS.

theorem NumberField.FinitePlace.norm_embedding {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : K) : ‖(embedding v) x‖ = (HeightOneSpectrum.adicAbv K 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_embedding' {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : K) : ‖(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_embedding_int (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : R) : ‖(embedding v) ((algebraMap R K) 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.

@[deprecated NumberField.FinitePlace.norm_embedding' (since := "2026-03-05")]

theorem NumberField.FinitePlace.norm_def' {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : K) : ‖(embedding v) x‖ = ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))

Alias of NumberField.FinitePlace.norm_embedding'.

---

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.

@[deprecated NumberField.FinitePlace.norm_embedding_int (since := "2026-03-05")]

theorem NumberField.FinitePlace.norm_def_int (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : R) : ‖(embedding v) ((algebraMap R K) x)‖ = ↑((WithZeroMulInt.toNNReal ⋯) (v.intValuation x))

Alias of NumberField.FinitePlace.norm_embedding_int.

---

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.FinitePlace.norm_le_one (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : R) : ‖(embedding v) ((algebraMap R K) 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] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : R) : ‖(embedding v) ((algebraMap R K) 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] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] (x : R) : ‖(embedding v) ((algebraMap R K) 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.

theorem NumberField.HeightOneSpectrum.embedding_mul_absNorm (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] {x : R} (h_x_nezero : x ≠ 0) : ‖(FinitePlace.embedding v) ((algebraMap R K) x)‖ * ↑(Ideal.absNorm (v.maxPowDividing (Ideal.span {x}))) = 1

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

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

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.

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

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

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

@[implicit_reducible]

instance NumberField.FinitePlace.instFunLikeReal {K : Type u_1} [Field K] [NumberField K] : FunLike (FinitePlace K) K ℝ

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 .

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

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.hasFiniteMulSupport_int {K : Type u_1} [Field K] [NumberField K] {x : RingOfIntegers K} (h_x_nezero : x ≠ 0) : Function.HasFiniteMulSupport fun (w : FinitePlace K) => w ↑x

@[deprecated NumberField.FinitePlace.hasFiniteMulSupport_int (since := "2026-03-03")]

theorem NumberField.FinitePlace.mulSupport_finite_int {K : Type u_1} [Field K] [NumberField K] {x : RingOfIntegers K} (h_x_nezero : x ≠ 0) : Function.HasFiniteMulSupport fun (w : FinitePlace K) => w ↑x

Alias of NumberField.FinitePlace.hasFiniteMulSupport_int.

theorem NumberField.FinitePlace.hasFiniteMulSupport {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) : Function.HasFiniteMulSupport fun (w : FinitePlace K) => w x

@[deprecated NumberField.FinitePlace.hasFiniteMulSupport (since := "2026-03-03")]

theorem NumberField.FinitePlace.mulSupport_finite {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) : Function.HasFiniteMulSupport fun (w : FinitePlace K) => w x

Alias of NumberField.FinitePlace.hasFiniteMulSupport.

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 NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : (equivHeightOneSpectrum.symm v) x = ‖(embedding v) x‖

@[deprecated NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply (since := "2026-03-11")]

theorem NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : (equivHeightOneSpectrum.symm v) x = ‖(embedding v) x‖

Alias of NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply.

@[deprecated NumberField.HeightOneSpectrum.embedding_mul_absNorm (since := "2026-03-11")]

theorem NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm (K : Type u_1) [Field K] {R : Type u_2} [CommRing R] [Algebra R K] [IsDedekindDomain R] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] {x : R} (h_x_nezero : x ≠ 0) : ‖(embedding v) ((algebraMap R K) x)‖ * ↑(Ideal.absNorm (v.maxPowDividing (Ideal.span {x}))) = 1

Alias of NumberField.HeightOneSpectrum.embedding_mul_absNorm.

instance NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers {K : Type u_1} [Field K] {L : Type u_3} [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)] [ContinuousSMul (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)] : Module.Finite (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)