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.

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] [IsDomain 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] [IsDomain 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] [IsDomain 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.instInhabitedFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain 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] [IsDomain 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] [IsDomain 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] [IsDomain 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.instTopologicalRingProdAdicCompletionsInstTopologicalSpaceProdAdicCompletionsInstNonUnitalNonAssocRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : TopologicalRing (DedekindDomain.ProdAdicCompletions R K)

Equations

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

instance DedekindDomain.instCommRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain 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] [IsDomain 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.instCoeFiniteIntegralAdelesProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Coe (DedekindDomain.FiniteIntegralAdeles R K) (DedekindDomain.ProdAdicCompletions R K)

Equations

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

theorem DedekindDomain.FiniteIntegralAdeles.coe_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain 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] [IsDomain 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] [IsDomain 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] [IsDomain 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] [IsDomain 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.instAlgebraProdAdicCompletionsToCommSemiringToSemifieldToSemiringToCommSemiringInstCommRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Algebra K (DedekindDomain.ProdAdicCompletions R K)

Equations

• DedekindDomain.instAlgebraProdAdicCompletionsToCommSemiringToSemifieldToSemiringToCommSemiringInstCommRingProdAdicCompletions R K = inferInstance

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

Equations

• DedekindDomain.ProdAdicCompletions.algebra' R K = inferInstance

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

Equations

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

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

Equations

• DedekindDomain.instAlgebraFiniteIntegralAdelesToCommSemiringToSemiringToCommSemiringInstCommRingFiniteIntegralAdeles R K = inferInstance

instance DedekindDomain.ProdAdicCompletions.algebraCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain 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 = RingHom.toAlgebra (DedekindDomain.FiniteIntegralAdeles.Coe.ringHom R K)

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

Equations

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

def DedekindDomain.FiniteIntegralAdeles.Coe.algHom (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain 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] [IsDomain 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] [IsDomain 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

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

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

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] [IsDomain 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] [IsDomain R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K} (hx : DedekindDomain.ProdAdicCompletions.IsFiniteAdele x) : DedekindDomain.ProdAdicCompletions.IsFiniteAdele (-x)

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] [IsDomain R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K} {y : DedekindDomain.ProdAdicCompletions R K} (hx : DedekindDomain.ProdAdicCompletions.IsFiniteAdele x) (hy : DedekindDomain.ProdAdicCompletions.IsFiniteAdele y) : DedekindDomain.ProdAdicCompletions.IsFiniteAdele (x * y)

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] [IsDomain R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : DedekindDomain.ProdAdicCompletions.IsFiniteAdele 1

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

noncomputable def DedekindDomain.finiteAdeleRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDomain R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Subring (DedekindDomain.ProdAdicCompletions R K)

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.

@[simp]

theorem DedekindDomain.mem_finiteAdeleRing_iff {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.ProdAdicCompletions R K) : x ∈ DedekindDomain.finiteAdeleRing R K ↔ DedekindDomain.ProdAdicCompletions.IsFiniteAdele x