mathlib3 documentation

ring_theory.dedekind_domain.finite_adele_ring

The finite adèle ring of a Dedekind domain #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. We define the ring of finite adèles of a Dedekind domain R.

Main definitions #

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 #

Tags #

finite adèle ring, dedekind domain

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 adic_completion with respect to adic_completion_integers. We prove that it is a commutative ring. TODO: show that it is a topological ring with the restricted product topology.

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

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

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

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

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

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

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

Equations