# 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 #

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

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

Equations
Instances For
instance DedekindDomain.instCommRingFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [] [] [] [Algebra 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) [] [] [] [Algebra 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) [] [] [] [Algebra R K] [] :
Equations
• =
instance DedekindDomain.instInhabitedFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [] [] [] [Algebra 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) [] [] [] [Algebra R K] [] :
Type (max u_1 u_2)

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

Equations
Instances For
instance DedekindDomain.instNonUnitalNonAssocRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra 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) [] [] [] [Algebra 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) [] [] [] [Algebra R K] [] :
Equations
• =
instance DedekindDomain.instCommRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
instance DedekindDomain.instInhabitedProdAdicCompletions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
noncomputable instance DedekindDomain.FiniteIntegralAdeles.instCoeProdAdicCompletions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• = { coe := fun (x : ) (v : ) => (x v) }
theorem DedekindDomain.FiniteIntegralAdeles.coe_apply (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] (x : ) :
(fun (v : ) => (x v)) v = (x v)
@[simp]
theorem DedekindDomain.FiniteIntegralAdeles.Coe.addMonoidHom_apply (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] (x : ) :
= (x v)
def DedekindDomain.FiniteIntegralAdeles.Coe.addMonoidHom (R : Type u_1) (K : Type u_2) [] [] [] [Algebra 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.
Instances For
@[simp]
theorem DedekindDomain.FiniteIntegralAdeles.Coe.ringHom_apply (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] (x : ) :
= (x v)
def DedekindDomain.FiniteIntegralAdeles.Coe.ringHom (R : Type u_1) (K : Type u_2) [] [] [] [Algebra 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.
Instances For
instance DedekindDomain.instAlgebraProdAdicCompletions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• = inferInstance
@[simp]
theorem DedekindDomain.ProdAdicCompletions.algebraMap_apply' (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] (k : K) :
() k v = K k
instance DedekindDomain.ProdAdicCompletions.algebra' (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• = inferInstance
@[simp]
theorem DedekindDomain.ProdAdicCompletions.algebraMap_apply (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] (r : R) :
() r v = K (() r)
instance DedekindDomain.instIsScalarTowerProdAdicCompletions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• =
instance DedekindDomain.instAlgebraFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• = inferInstance
instance DedekindDomain.ProdAdicCompletions.algebraCompletions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
instance DedekindDomain.ProdAdicCompletions.isScalarTower_completions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• =
def DedekindDomain.FiniteIntegralAdeles.Coe.algHom (R : Type u_1) (K : Type u_2) [] [] [] [Algebra 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.
Instances For
theorem DedekindDomain.FiniteIntegralAdeles.Coe.algHom_apply (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] (x : ) :
= (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} [] [] [] [Algebra R K] [] (x : ) :

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 : ) in Filter.cofinite,
Instances For
theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.add {R : Type u_1} {K : Type u_2} [] [] [] [Algebra R K] [] {x : } {y : } (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) :

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.zero {R : Type u_1} {K : Type u_2} [] [] [] [Algebra R K] [] :

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

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

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

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.one {R : Type u_1} {K : Type u_2} [] [] [] [Algebra R K] [] :

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

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.algebraMap' {R : Type u_1} {K : Type u_2} [] [] [] [Algebra R K] [] (k : K) :
def DedekindDomain.FiniteAdeleRing (R : Type u_1) (K : Type u_2) [] [] [] [Algebra 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance DedekindDomain.FiniteAdeleRing.instCommRing (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• One or more equations did not get rendered due to their size.
instance DedekindDomain.FiniteAdeleRing.instAlgebra (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• One or more equations did not get rendered due to their size.
instance DedekindDomain.FiniteAdeleRing.instCoeProdAdicCompletions (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] :
Equations
• = { coe := fun (x : ) => x }
theorem DedekindDomain.FiniteAdeleRing.ext (R : Type u_1) (K : Type u_2) [] [] [] [Algebra R K] [] {a₁ : } {a₂ : } (h : a₁ = a₂) :
a₁ = a₂