The finite adèle ring of a Dedekind domain

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

Main definitions

• IsDedekindDomain.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öhlich, Algebraic Number Theory][cassels1967algebraic]

Tags

finite adèle ring, dedekind domain

def IsDedekindDomain.HeightOneSpectrum.Support (R : Type u_1) [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (k : K) : Set (HeightOneSpectrum R)

The support of an element k of the field of fractions of a Dedekind domain is the set of maximal ideals of the Dedekind domain at which k is not integral.

Equations

• IsDedekindDomain.HeightOneSpectrum.Support R k = {v : IsDedekindDomain.HeightOneSpectrum R | 1 < (IsDedekindDomain.HeightOneSpectrum.valuation K v) k}

theorem IsDedekindDomain.HeightOneSpectrum.Support.finite (R : Type u_1) [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (k : K) : (Support R k).Finite

The support of an element of the field of fractions of a Dedekind domain is finite.

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.

@[reducible, inline]

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

If K is the field of fractions of the Dedekind domain R then FiniteAdeleRing R K is the ring of finite adeles of K, defined as the restricted product of the completions K_v with respect to the subrings R_v. Here v runs through the nonzero primes of R and the restricted product is the subring of ∏_v K_v consisting of elements which are in R_v for all but finitely many v.

Equations

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

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

The canonical map from K to the finite adeles of K.

The content of the existence of this map is the fact that an element k of K is integral at all but finitely many places, which is IsDedekindDomain.HeightOneSpectrum.Support.finite R k.

Equations

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

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

Equations

• IsDedekindDomain.FiniteAdeleRing.instAlgebra R K = (IsDedekindDomain.FiniteAdeleRing.algebraMap R K).toAlgebra

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

Equations

• IsDedekindDomain.FiniteAdeleRing.instAlgebra_1 R K = Algebra.compHom (IsDedekindDomain.FiniteAdeleRing R K) (algebraMap R K)

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

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

theorem IsDedekindDomain.FiniteAdeleRing.ext_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {a₁ a₂ : FiniteAdeleRing R K} : a₁ = a₂ ↔ ∀ (v : HeightOneSpectrum R), a₁ v = a₂ v

instance IsDedekindDomain.FiniteAdeleRing.instDFunLikeHeightOneSpectrumAdicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : DFunLike (FiniteAdeleRing R K) (HeightOneSpectrum R) (HeightOneSpectrum.adicCompletion K)

Equations

• IsDedekindDomain.FiniteAdeleRing.instDFunLikeHeightOneSpectrumAdicCompletion R K = { coe := fun (a : IsDedekindDomain.FiniteAdeleRing R K) => ↑a, coe_injective' := ⋯ }

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