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 in Mathlib.RingTheory.DedekindDomain.finiteAdeleRing https://github.com/leanprover-community/mathlib4/blob/1c0ac885c9b8aa4daa1830acb56b755140a8059f/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean#L274-L280. In this file we supplement the theory by defining some local maps and the topological space for the finite adele ring.

Main definitions #

DedekindDomain.FiniteAdeleRing.projection v is the map sending a finite adele x to its vth place x v in the v-adic completion of K.
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.
DedekindDomain.FiniteAdeleRing.generatingSet is the generating set of the topology of the finite adele ring.

Main results #

DedekindDomain.FiniteAdeleRing.continuous_if_factors₂ : Any map on the product of the finite adele ring to the finite adele ring is continuous if it factors through continuous maps at each place v, each of which preserve the integers.
DedekindDomain.FiniteAdeleRing.topologicalRing : the topological ring structure on the finite adele ring.

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

source

def DedekindDomain.ProdAdicCompletions.globalEmbedding (R : Type u_1) [CommRing R] [IsDomain 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 = Pi.ringHom fun (v : IsDedekindDomain.HeightOneSpectrum R) => IsDedekindDomain.HeightOneSpectrum.AdicCompletion.coeRingHom K v

Instances For

source

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

DedekindDomain.ProdAdicCompletions R K →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

Sends an element of the product of all adicCompletions to a local place.

Equations

DedekindDomain.ProdAdicCompletions.projection K v = Pi.evalRingHom (fun (v : IsDedekindDomain.HeightOneSpectrum R) => IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) v

Instances For

source

def DedekindDomain.ProdAdicCompletions.localInclusion {R : Type u_1} [CommRing R] [IsDomain 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

Instances For

source

theorem DedekindDomain.ProdAdicCompletions.isFiniteAdele_localInclusion {R : Type u_1} [CommRing R] [IsDomain 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.IsFiniteAdele (DedekindDomain.ProdAdicCompletions.localInclusion K v x)

The local inclusion of any element is a finite adele.

source

theorem DedekindDomain.ProdAdicCompletions.localInclusion_rfl {R : Type u_1} [CommRing R] [IsDomain 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.

source

theorem DedekindDomain.ProdAdicCompletions.projection_localInclusion_eq {R : Type u_1} [CommRing R] [IsDomain 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.projection K v) (DedekindDomain.ProdAdicCompletions.localInclusion K v x) = x

The projection and local inclusions are inverses on ProdAdicCompletions.

source

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

↥(DedekindDomain.finiteAdeleRing R K) →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

Sends a finite adele to a local place.

Equations

DedekindDomain.FiniteAdeleRing.projection K v = RingHom.comp (Pi.evalRingHom (IsDedekindDomain.HeightOneSpectrum.adicCompletion K) v) (Subring.subtype (DedekindDomain.finiteAdeleRing R K))

Instances For

source

def DedekindDomain.FiniteAdeleRing.localInclusion {R : Type u_1} [CommRing R] [IsDomain 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 = { val := DedekindDomain.ProdAdicCompletions.localInclusion K v x, property := ⋯ }

Instances For

source

theorem DedekindDomain.FiniteAdeleRing.localInclusion_rfl {R : Type u_1} [CommRing R] [IsDomain 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.

source

theorem DedekindDomain.FiniteAdeleRing.projection_localInclusion_eq {R : Type u_1} [CommRing R] [IsDomain 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.projection K v) (DedekindDomain.FiniteAdeleRing.localInclusion K v x) = x

The projection and local inclusions are inverses on the finite adele ring.

source

def DedekindDomain.FiniteAdeleRing.generatingSet (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] :

Set (Set ↥(DedekindDomain.finiteAdeleRing R K))

The generating set of the finite adele ring are all sets of the form Πᵥ Vᵥ, where each Vᵥ is open in Kᵥ and for all but finitely many v we have that Vᵥ is the v-adic ring of integers.

Equations

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

Instances For

source

instance DedekindDomain.FiniteAdeleRing.topologicalSpace (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] :

TopologicalSpace ↥(DedekindDomain.finiteAdeleRing R K)

Equations

DedekindDomain.FiniteAdeleRing.topologicalSpace R K = TopologicalSpace.generateFrom (DedekindDomain.FiniteAdeleRing.generatingSet R K)

source

∃ (X : Set ↥(DedekindDomain.finiteAdeleRing R K)) (Y : Set ↥(DedekindDomain.finiteAdeleRing R K)), IsOpen X ∧ IsOpen Y ∧ x ∈ X ∧ y ∈ Y ∧ X ×ˢ Y ⊆ f ⁻¹' U

Consider two finite adeles x, y, a generating open set U of the finite adele ring and a functionf : finiteAdeleRing R K × finiteAdeleRing R K → finiteAdeleRing K such that (x, y) is in the preimage of U under f. If f factors through a collection of continuous maps g v defined at each place, which each preserve the respective ring of integers, then we can obtain two open sets X and Y of the finite adele ring, which contain x and y respectively, such that their product X ×ˢ Y is contained in the preimage of U under f.

Abstracted version of https://github.com/mariainesdff/ideles/blob/e6646cd462c86a8813ca04fb82e84cdc14a59ad4/src/adeles_R.lean#L469

source

Continuous f

If f : finiteAdeleRing R K × finiteAdeleRing R K → finiteAdeleRing R K factors through a collection of continuous maps g v defined at each place, which each preserve the respective ring of integers, then f is continuous.

source