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.vadicAbv: a v-adic absolute value on K.
• NumberField.FinitePlace: the type of finite places of a number field K.
• 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

theorem NumberField.one_lt_norm {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.one_lt_norm_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.norm_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.vadicAbv {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.vadicAbv v = { toFun := fun (x : K) => ↑((WithZeroMulInt.toNNReal ⋯) (v.valuation x)), map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

theorem NumberField.vadicAbv_def {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {x : K} : (vadicAbv v) x = ↑((WithZeroMulInt.toNNReal ⋯) (v.valuation x))

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

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

Equations

• NumberField.embedding v = UniformSpace.Completion.coeRingHom

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

Equations

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

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

• NumberField.FinitePlace K = { w : AbsoluteValue K ℝ // ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), NumberField.place (NumberField.embedding v) = w }

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.embedding v), ⋯⟩

theorem NumberField.toNNReal_Valued_eq_vadicAbv {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : ↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x)) = (vadicAbv v) x

theorem NumberField.FinitePlace.norm_def {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : ‖(embedding v) x‖ = (vadicAbv 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 : K) : ‖(embedding v) x‖ = ↑((WithZeroMulInt.toNNReal ⋯) (v.valuation 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 K) : ‖(embedding v) ↑x‖ = ↑((WithZeroMulInt.toNNReal ⋯) (v.intValuationDef 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.norm_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers K) : ‖(embedding v) ↑x‖ ≤ 1

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

theorem NumberField.norm_eq_one_iff_not_mem {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers K) : ‖(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.norm_lt_one_iff_mem {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : RingOfIntegers K) : ‖(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.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.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 K} (h_x_nezero : x ≠ 0) : ‖(NumberField.embedding v) ↑x‖ * ↑(Ideal.absNorm (v.maxPowDividing (Ideal.span {x}))) = 1