The finite adèle ring of a Dedekind domain

We define the ring of finite adèles of a Dedekind domain R.

Main definitions

• DedekindDomain.FiniteIntegralAdeles : product of adicCompletionIntegers, where v runs over all maximal ideals of R.
• DedekindDomain.ProdAdicCompletions : the product of adicCompletion, where v runs over all maximal ideals of R.
• DedekindDomain.finiteAdeleRing : The finite adèle ring of R, defined as the restricted product Π'_v K_v. We give this ring a K-algebra structure.

Implementation notes

We are only interested on Dedekind domains of Krull dimension 1 (i.e., not fields). If R is a field, its finite adèle ring is just defined to be the trivial ring.

References

• [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]

Tags

finite adèle ring, dedekind domain

def DedekindDomain.FiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Type (max u_1 u_2)

The product of all adicCompletionIntegers, where v runs over the maximal ideals of R.

Equations

• DedekindDomain.FiniteIntegralAdeles R K = ((v : IsDedekindDomain.HeightOneSpectrum R) → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))

instance DedekindDomain.instCommRingFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : CommRing (DedekindDomain.FiniteIntegralAdeles R K)

Equations

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

instance DedekindDomain.instTopologicalSpaceFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : TopologicalSpace (DedekindDomain.FiniteIntegralAdeles R K)

Equations

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

instance DedekindDomain.instTopologicalRingFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : TopologicalRing (DedekindDomain.FiniteIntegralAdeles R K)

Equations

• ⋯ = ⋯

instance DedekindDomain.instInhabitedFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Inhabited (DedekindDomain.FiniteIntegralAdeles R K)

Equations

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

def DedekindDomain.ProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Type (max u_1 u_2)

The product of all adicCompletion, where v runs over the maximal ideals of R.

Equations

• DedekindDomain.ProdAdicCompletions R K = ((v : IsDedekindDomain.HeightOneSpectrum R) → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

instance DedekindDomain.instNonUnitalNonAssocRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : NonUnitalNonAssocRing (DedekindDomain.ProdAdicCompletions R K)

Equations

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

instance DedekindDomain.instTopologicalSpaceProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : TopologicalSpace (DedekindDomain.ProdAdicCompletions R K)

Equations

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

instance DedekindDomain.instTopologicalRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : TopologicalRing (DedekindDomain.ProdAdicCompletions R K)

Equations

• ⋯ = ⋯

instance DedekindDomain.instCommRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : CommRing (DedekindDomain.ProdAdicCompletions R K)

Equations

• DedekindDomain.instCommRingProdAdicCompletions R K = inferInstanceAs (CommRing ((v : IsDedekindDomain.HeightOneSpectrum R) → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

instance DedekindDomain.instInhabitedProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Inhabited (DedekindDomain.ProdAdicCompletions R K)

Equations

• DedekindDomain.instInhabitedProdAdicCompletions R K = inferInstanceAs (Inhabited ((v : IsDedekindDomain.HeightOneSpectrum R) → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

noncomputable instance DedekindDomain.FiniteIntegralAdeles.instCoeProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Coe (DedekindDomain.FiniteIntegralAdeles R K) (DedekindDomain.ProdAdicCompletions R K)

Equations

• DedekindDomain.FiniteIntegralAdeles.instCoeProdAdicCompletions R K = { coe := fun (x : DedekindDomain.FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) => ↑(x v) }

theorem DedekindDomain.FiniteIntegralAdeles.coe_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) : (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑(x v)) v = ↑(x v)

@[simp]

theorem DedekindDomain.FiniteIntegralAdeles.Coe.addMonoidHom_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) : (DedekindDomain.FiniteIntegralAdeles.Coe.addMonoidHom R K) x v = ↑(x v)

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

The inclusion of R_hat in K_hat as a homomorphism of additive monoids.

Equations

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

@[simp]

theorem DedekindDomain.FiniteIntegralAdeles.Coe.ringHom_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) : (DedekindDomain.FiniteIntegralAdeles.Coe.ringHom R K) x v = ↑(x v)

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

The inclusion of R_hat in K_hat as a ring homomorphism.

Equations

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

instance DedekindDomain.instAlgebraProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Algebra K (DedekindDomain.ProdAdicCompletions R K)

Equations

• DedekindDomain.instAlgebraProdAdicCompletions R K = inferInstance

@[simp]

theorem DedekindDomain.ProdAdicCompletions.algebraMap_apply' (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (k : K) : (algebraMap K (DedekindDomain.ProdAdicCompletions R K)) k v = ↑K k

instance DedekindDomain.ProdAdicCompletions.algebra' (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Algebra R (DedekindDomain.ProdAdicCompletions R K)

Equations

• DedekindDomain.ProdAdicCompletions.algebra' R K = inferInstance

@[simp]

theorem DedekindDomain.ProdAdicCompletions.algebraMap_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : (algebraMap R (DedekindDomain.ProdAdicCompletions R K)) r v = ↑K ((algebraMap R K) r)

instance DedekindDomain.instIsScalarTowerProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsScalarTower R K (DedekindDomain.ProdAdicCompletions R K)

Equations

• ⋯ = ⋯

instance DedekindDomain.instAlgebraFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Algebra R (DedekindDomain.FiniteIntegralAdeles R K)

Equations

• DedekindDomain.instAlgebraFiniteIntegralAdeles R K = inferInstance

instance DedekindDomain.ProdAdicCompletions.algebraCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Algebra (DedekindDomain.FiniteIntegralAdeles R K) (DedekindDomain.ProdAdicCompletions R K)

Equations

• DedekindDomain.ProdAdicCompletions.algebraCompletions R K = (DedekindDomain.FiniteIntegralAdeles.Coe.ringHom R K).toAlgebra

instance DedekindDomain.ProdAdicCompletions.isScalarTower_completions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsScalarTower R (DedekindDomain.FiniteIntegralAdeles R K) (DedekindDomain.ProdAdicCompletions R K)

Equations

• ⋯ = ⋯

def DedekindDomain.FiniteIntegralAdeles.Coe.algHom (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : DedekindDomain.FiniteIntegralAdeles R K →ₐ[R] DedekindDomain.ProdAdicCompletions R K

The inclusion of R_hat in K_hat as an algebra homomorphism.

Equations

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

theorem DedekindDomain.FiniteIntegralAdeles.Coe.algHom_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) : (DedekindDomain.FiniteIntegralAdeles.Coe.algHom R K) x v = ↑(x v)

The finite adèle ring of a Dedekind domain

We define the finite adèle ring of R as the restricted product over all maximal ideals v of R of adicCompletion with respect to adicCompletionIntegers. We prove that it is a commutative ring. TODO: show that it is a topological ring with the restricted product topology.

def DedekindDomain.ProdAdicCompletions.IsFiniteAdele {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.ProdAdicCompletions R K) : Prop

An element x : K_hat R K is a finite adèle if for all but finitely many height one ideals v, the component x v is a v-adic integer.

Equations

• x.IsFiniteAdele = ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, x v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

@[simp]

theorem DedekindDomain.ProdAdicCompletions.isFiniteAdele_iff {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.ProdAdicCompletions R K) : x.IsFiniteAdele ↔ {v : IsDedekindDomain.HeightOneSpectrum R | x v ∉ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v}.Finite

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.add {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K} {y : DedekindDomain.ProdAdicCompletions R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) : (x + y).IsFiniteAdele

The sum of two finite adèles is a finite adèle.

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.zero {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : DedekindDomain.ProdAdicCompletions.IsFiniteAdele 0

The tuple (0)_v is a finite adèle.

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.neg {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K} (hx : x.IsFiniteAdele) : (-x).IsFiniteAdele

The negative of a finite adèle is a finite adèle.

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.mul {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K} {y : DedekindDomain.ProdAdicCompletions R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) : (x * y).IsFiniteAdele

The product of two finite adèles is a finite adèle.

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.one {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : DedekindDomain.ProdAdicCompletions.IsFiniteAdele 1

The tuple (1)_v is a finite adèle.

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.algebraMap' {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (k : K) : ((algebraMap K (DedekindDomain.ProdAdicCompletions R K)) k).IsFiniteAdele

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

The finite adèle ring of R is the restricted product over all maximal ideals v of R of adicCompletion, with respect to adicCompletionIntegers.

Note that we make this a Type rather than a Subtype (e.g., a subalgebra) since we wish to endow it with a finer topology than that of the subspace topology.

Equations

• DedekindDomain.FiniteAdeleRing R K = { x : DedekindDomain.ProdAdicCompletions R K // x.IsFiniteAdele }

def DedekindDomain.FiniteAdeleRing.subalgebra (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Subalgebra K (DedekindDomain.ProdAdicCompletions R K)

The finite adèle ring of R, regarded as a K-subalgebra of the product of the local completions of K.

Note that this definition exists to streamline the proof that the finite adèles are an algebra over K, rather than to express their relationship to K_hat R K which is essentially a detail of their construction.

Equations

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

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

Equations

• DedekindDomain.FiniteAdeleRing.instCommRing R K = (DedekindDomain.FiniteAdeleRing.subalgebra R K).toCommRing

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

Equations

• DedekindDomain.FiniteAdeleRing.instAlgebra R K = (DedekindDomain.FiniteAdeleRing.subalgebra R K).algebra

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

Equations

• DedekindDomain.FiniteAdeleRing.instAlgebra_1 R K = ((algebraMap K (DedekindDomain.FiniteAdeleRing R K)).comp (algebraMap R K)).toAlgebra

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

Equations

• ⋯ = ⋯

instance DedekindDomain.FiniteAdeleRing.instCoeProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Coe (DedekindDomain.FiniteAdeleRing R K) (DedekindDomain.ProdAdicCompletions R K)

Equations

• DedekindDomain.FiniteAdeleRing.instCoeProdAdicCompletions R K = { coe := fun (x : DedekindDomain.FiniteAdeleRing R K) => ↑x }

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

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

The finite adele ring is an algebra over the finite integral adeles.

Equations

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

instance DedekindDomain.FiniteAdeleRing.instCoeFunForallAdicCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : CoeFun (DedekindDomain.FiniteAdeleRing R K) fun (x : DedekindDomain.FiniteAdeleRing R K) => (v : IsDedekindDomain.HeightOneSpectrum R) → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

Equations

• DedekindDomain.FiniteAdeleRing.instCoeFunForallAdicCompletion R K = { coe := fun (a : DedekindDomain.FiniteAdeleRing R K) (v : IsDedekindDomain.HeightOneSpectrum R) => ↑a v }

theorem DedekindDomain.FiniteAdeleRing.exists_finiteIntegralAdele_iff {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (a : DedekindDomain.FiniteAdeleRing R K) : (∃ (c : DedekindDomain.FiniteIntegralAdeles R K), a = ↑c) ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑a v) v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

theorem DedekindDomain.FiniteAdeleRing.mul_nonZeroDivisor_mem_finiteIntegralAdeles {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (a : DedekindDomain.FiniteAdeleRing R K) : ∃ (b : ↥(nonZeroDivisors R)) (c : DedekindDomain.FiniteIntegralAdeles R K), a * ↑↑b = ↑c

theorem DedekindDomain.FiniteAdeleRing.submodulesRingBasis (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : SubmodulesRingBasis fun (r : ↥(nonZeroDivisors R)) => Submodule.span (DedekindDomain.FiniteIntegralAdeles R K) {↑↑r}

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

Equations

• DedekindDomain.FiniteAdeleRing.instTopologicalSpace R K = ⋯.topology