Finite adele ring

Let R be a Dedekind domain of Krull dimension 1, K its field of fractions. The finite adele ring of K is defined as a topological ring in Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing. In this file we supplement the theory by defining some local and global maps, and helper results for working with the topological space of the the finite adele ring.

Main definitions

• DedekindDomain.FiniteAdeleRing.localInclusion v is the map sending an element x of the v-adic completion of K to the finite adele which has x in its vth place and 1s everywhere else.

Main results

• DedekindDomain.FiniteAdeleRing.dvd_of_valued_lt : a finite adele is an ∏ v, Oᵥ multiple of an integer r if the valuation of x v is less than the valuation of r for every v dividing r.
• DedekindDomain.FiniteAdeleRing.exists_not_mem_of_finite_nhds : there exists a finite adele whose valuation is outside a finite collection of open balls.

References

• [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
• [M.I. de Frutos-Fernàndez, Formalizing the Ring of Adèles of a Global Field][defrutosfernandez2022]

Tags

finite adele ring, dedekind domain

def DedekindDomain.ProdAdicCompletions.globalEmbedding (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : K →+* DedekindDomain.ProdAdicCompletions R K

Equations

• DedekindDomain.ProdAdicCompletions.globalEmbedding R K = algebraMap K (DedekindDomain.ProdAdicCompletions R K)

@[simp]

theorem DedekindDomain.ProdAdicCompletions.globalEmbedding_apply (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : K) : (DedekindDomain.ProdAdicCompletions.globalEmbedding R K) x v = ↑K x

def DedekindDomain.ProdAdicCompletions.localInclusion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v → DedekindDomain.ProdAdicCompletions R K

Sends a local element to the product of all adicCompletions filled with 1s elsewhere.

Equations

• DedekindDomain.ProdAdicCompletions.localInclusion K v x w = if hw : w = v then ⋯ ▸ x else 1

theorem DedekindDomain.ProdAdicCompletions.localInclusion_isFiniteAdele {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) : (DedekindDomain.ProdAdicCompletions.localInclusion K v x).IsFiniteAdele

The local inclusion of any element is a finite adele.

@[simp]

theorem DedekindDomain.ProdAdicCompletions.localInclusion_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) : DedekindDomain.ProdAdicCompletions.localInclusion K v x v = x

The vth place of the local inclusion is the original element.

@[simp]

theorem DedekindDomain.ProdAdicCompletions.localInclusion_apply' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {w : IsDedekindDomain.HeightOneSpectrum R} (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (h : w ≠ v) : DedekindDomain.ProdAdicCompletions.localInclusion K v x w = 1

@[simp]

theorem DedekindDomain.FiniteAdeleRing.smul_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : DedekindDomain.FiniteIntegralAdeles R K) (y : DedekindDomain.FiniteAdeleRing R K) : (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑(x • y) v) v = ↑(x v) * (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑y v) v

@[simp]

theorem DedekindDomain.FiniteAdeleRing.add_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : DedekindDomain.FiniteAdeleRing R K) (y : DedekindDomain.FiniteAdeleRing R K) : (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑(x + y) v) v = (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑x v) v + (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑y v) v

@[simp]

theorem DedekindDomain.FiniteAdeleRing.sub_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : DedekindDomain.FiniteAdeleRing R K) (y : DedekindDomain.FiniteAdeleRing R K) : (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑(x - y) v) v = (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑x v) v - (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑y v) v

@[simp]

theorem DedekindDomain.FiniteAdeleRing.mul_integer_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : DedekindDomain.FiniteAdeleRing R K) (r : R) : (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑(x * (algebraMap R (DedekindDomain.FiniteAdeleRing R K)) r) v) v = (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑x v) v * (algebraMap R (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) r

def DedekindDomain.FiniteAdeleRing.localInclusion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v → DedekindDomain.FiniteAdeleRing R K

Sends a local element to a finite adele filled with 1s elsewhere.

Equations

• DedekindDomain.FiniteAdeleRing.localInclusion K v x = ⟨DedekindDomain.ProdAdicCompletions.localInclusion K v x, ⋯⟩

@[simp]

theorem DedekindDomain.FiniteAdeleRing.localInclusion_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) : ↑(DedekindDomain.FiniteAdeleRing.localInclusion K v x) v = x

The vth place of the local inclusion is the original element.

@[simp]

theorem DedekindDomain.FiniteAdeleRing.localInclusion_apply' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (w : IsDedekindDomain.HeightOneSpectrum R) (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (h : w ≠ v) : ↑(DedekindDomain.FiniteAdeleRing.localInclusion K v x) w = 1

def DedekindDomain.FiniteAdeleRing.support {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.FiniteAdeleRing R K) : Finset (IsDedekindDomain.HeightOneSpectrum R)

Equations

• x.support = ⋯.toFinset

theorem DedekindDomain.FiniteAdeleRing.exists_not_mem_of_finite_nhds {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (γ : IsDedekindDomain.HeightOneSpectrum R → (WithZero (Multiplicative ℤ))ˣ) (y : DedekindDomain.FiniteAdeleRing R K) : ∃ (x : DedekindDomain.FiniteAdeleRing R K), ∀ v ∈ S, Valued.v ((fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑x v) v - (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑y v) v) > ↑(γ v)

Given balls centred at yᵥ of radius γᵥ for a finite set of primes v ∈ S, we can find a finite adele x for which xᵥ is outside each open ball for v ∈ S.

theorem DedekindDomain.FiniteAdeleRing.sub_mul_nonZeroDivisor_mem_finiteIntegralAdeles {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.FiniteAdeleRing R K) (y : DedekindDomain.FiniteAdeleRing R K) : ∃ (r : ↥(nonZeroDivisors R)) (z : DedekindDomain.FiniteIntegralAdeles R K), (y - x) * (algebraMap R (DedekindDomain.FiniteAdeleRing R K)) ↑r = (algebraMap (DedekindDomain.FiniteIntegralAdeles R K) (DedekindDomain.FiniteAdeleRing R K)) z

Clears the denominator of the subtraction of two finite adeles.

theorem DedekindDomain.FiniteAdeleRing.dvd_of_valued_lt {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.FiniteAdeleRing R K} {r : ↥(nonZeroDivisors R)} {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} (hS : ∀ (v : IsDedekindDomain.HeightOneSpectrum R), v.asIdeal ∣ Ideal.span {↑r} → v ∈ S) (hvS : ∀ v ∈ S, Valued.v ((fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑x v) v) < Valued.v ((algebraMap R (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ↑r)) (hvnS : ∀ v ∉ S, (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑x v) v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) : ∃ (a : DedekindDomain.FiniteIntegralAdeles R K), a • (algebraMap R (DedekindDomain.FiniteAdeleRing R K)) ↑r = x

Let x be a finite adele and let r be a non-zero integral divisor. If, for some finite set of primes v ∈ S containing the factors of r, the valuation of xᵥ is less than the valuation of r, then x is an integral multiple of the global embedding of r.

@[simp]

theorem DedekindDomain.FiniteAdeleRing.algebraMap_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : K) : (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑((algebraMap K (DedekindDomain.FiniteAdeleRing R K)) x) v) v = ↑K x

theorem DedekindDomain.FiniteAdeleRing.ext_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {a₁ : DedekindDomain.FiniteAdeleRing R K} {a₂ : DedekindDomain.FiniteAdeleRing R K} : a₁ = a₂ ↔ ↑a₁ = ↑a₂

theorem DedekindDomain.FiniteAdeleRing.nontrivial_of_nonEmpty (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [i : Nonempty (IsDedekindDomain.HeightOneSpectrum R)] : Nontrivial (DedekindDomain.FiniteAdeleRing R K)

theorem DedekindDomain.FiniteAdeleRing.algebraMap_injective (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [i : Nonempty (IsDedekindDomain.HeightOneSpectrum R)] : Function.Injective ⇑(algebraMap K (DedekindDomain.FiniteAdeleRing R K))