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 #

dedekind_domain.finite_integral_adeles : product of adic_completion_integers, where v runs over all maximal ideals of R.
dedekind_domain.prod_adic_completions : the product of adic_completion, where v runs over all maximal ideals of R.
dedekind_domain.finite_adele_ring : 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

Tags #

finite adèle ring, dedekind domain

source

@[protected, instance]

noncomputable def dedekind_domain.finite_integral_adeles.comm_ring (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

comm_ring (dedekind_domain.finite_integral_adeles R K)

source

@[protected, instance]

noncomputable def dedekind_domain.finite_integral_adeles.inhabited (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inhabited (dedekind_domain.finite_integral_adeles R K)

source

@[protected, instance]

noncomputable def dedekind_domain.finite_integral_adeles.topological_space (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_space (dedekind_domain.finite_integral_adeles R K)

source

def dedekind_domain.finite_integral_adeles (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

Type (max u_1 u_2)

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

Equations

dedekind_domain.finite_integral_adeles R K = Π (v : is_dedekind_domain.height_one_spectrum R), ↥(is_dedekind_domain.height_one_spectrum.adic_completion_integers K v)

Instances for dedekind_domain.finite_integral_adeles

source

@[protected, instance]

def dedekind_domain.prod_adic_completions.topological_ring (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_ring (dedekind_domain.prod_adic_completions R K)

source

def dedekind_domain.prod_adic_completions (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

Type (max u_1 u_2)

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

Equations

dedekind_domain.prod_adic_completions R K = Π (v : is_dedekind_domain.height_one_spectrum R), is_dedekind_domain.height_one_spectrum.adic_completion K v

Instances for dedekind_domain.prod_adic_completions

source

@[protected, instance]

noncomputable def dedekind_domain.prod_adic_completions.inhabited (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inhabited (dedekind_domain.prod_adic_completions R K)

source

@[protected, instance]

noncomputable def dedekind_domain.prod_adic_completions.topological_space (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_space (dedekind_domain.prod_adic_completions R K)

source

@[protected, instance]

noncomputable def dedekind_domain.prod_adic_completions.comm_ring (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

comm_ring (dedekind_domain.prod_adic_completions R K)

source

@[protected, instance]

noncomputable def dedekind_domain.prod_adic_completions.non_unital_non_assoc_ring (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

non_unital_non_assoc_ring (dedekind_domain.prod_adic_completions R K)

source

@[protected, instance]

def dedekind_domain.finite_integral_adeles.dedekind_domain.prod_adic_completions.has_coe (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

has_coe (dedekind_domain.finite_integral_adeles R K) (dedekind_domain.prod_adic_completions R K)

Equations

dedekind_domain.finite_integral_adeles.dedekind_domain.prod_adic_completions.has_coe R K = {coe := λ (x : dedekind_domain.finite_integral_adeles R K) (v : is_dedekind_domain.height_one_spectrum R), ↑(x v)}

source

theorem dedekind_domain.finite_integral_adeles.coe_apply (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : dedekind_domain.finite_integral_adeles R K) (v : is_dedekind_domain.height_one_spectrum R) :

↑x v = ↑(x v)

source

@[simp]

theorem dedekind_domain.finite_integral_adeles.coe.add_monoid_hom_apply (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (ᾰ : dedekind_domain.finite_integral_adeles R K) :

⇑(dedekind_domain.finite_integral_adeles.coe.add_monoid_hom R K) ᾰ = ↑ᾰ

source

noncomputable def dedekind_domain.finite_integral_adeles.coe.add_monoid_hom (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

dedekind_domain.finite_integral_adeles R K →+ dedekind_domain.prod_adic_completions R K

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

Equations

dedekind_domain.finite_integral_adeles.coe.add_monoid_hom R K = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

source

@[simp]

theorem dedekind_domain.finite_integral_adeles.coe.ring_hom_apply (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (ᾰ : dedekind_domain.finite_integral_adeles R K) :

⇑(dedekind_domain.finite_integral_adeles.coe.ring_hom R K) ᾰ = ↑ᾰ

source

noncomputable def dedekind_domain.finite_integral_adeles.coe.ring_hom (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

dedekind_domain.finite_integral_adeles R K →+* dedekind_domain.prod_adic_completions R K

The inclusion of R_hat in K_hat as a ring homomorphism.

Equations

dedekind_domain.finite_integral_adeles.coe.ring_hom R K = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[protected, instance]

noncomputable def dedekind_domain.prod_adic_completions.algebra (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

algebra K (dedekind_domain.prod_adic_completions R K)

Equations

dedekind_domain.prod_adic_completions.algebra R K = pi.algebra (is_dedekind_domain.height_one_spectrum R) (λ (v : is_dedekind_domain.height_one_spectrum R), is_dedekind_domain.height_one_spectrum.adic_completion K v)

source

@[protected, instance]

noncomputable def dedekind_domain.prod_adic_completions.algebra' (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

algebra R (dedekind_domain.prod_adic_completions R K)

Equations

dedekind_domain.prod_adic_completions.algebra' R K = pi.algebra (is_dedekind_domain.height_one_spectrum R) (λ (v : is_dedekind_domain.height_one_spectrum R), is_dedekind_domain.height_one_spectrum.adic_completion K v)

source

@[protected, instance]

def dedekind_domain.prod_adic_completions.is_scalar_tower (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

is_scalar_tower R K (dedekind_domain.prod_adic_completions R K)

source

@[protected, instance]

noncomputable def dedekind_domain.finite_integral_adeles.algebra (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

algebra R (dedekind_domain.finite_integral_adeles R K)

Equations

dedekind_domain.finite_integral_adeles.algebra R K = pi.algebra (is_dedekind_domain.height_one_spectrum R) (λ (v : is_dedekind_domain.height_one_spectrum R), ↥(is_dedekind_domain.height_one_spectrum.adic_completion_integers K v))

source

@[protected, instance]

noncomputable def dedekind_domain.prod_adic_completions.algebra_completions (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

algebra (dedekind_domain.finite_integral_adeles R K) (dedekind_domain.prod_adic_completions R K)

Equations

dedekind_domain.prod_adic_completions.algebra_completions R K = (dedekind_domain.finite_integral_adeles.coe.ring_hom R K).to_algebra

source

@[protected, instance]

def dedekind_domain.prod_adic_completions.is_scalar_tower_completions (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

is_scalar_tower R (dedekind_domain.finite_integral_adeles R K) (dedekind_domain.prod_adic_completions R K)

source

noncomputable def dedekind_domain.finite_integral_adeles.coe.alg_hom (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

dedekind_domain.finite_integral_adeles R K →ₐ[R] dedekind_domain.prod_adic_completions R K

The inclusion of R_hat in K_hat as an algebra homomorphism.

Equations

dedekind_domain.finite_integral_adeles.coe.alg_hom R K = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

theorem dedekind_domain.finite_integral_adeles.coe.alg_hom_apply (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : dedekind_domain.finite_integral_adeles R K) (v : is_dedekind_domain.height_one_spectrum R) :

⇑(dedekind_domain.finite_integral_adeles.coe.alg_hom 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 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.

source

def dedekind_domain.prod_adic_completions.is_finite_adele {R : Type u_1} {K : Type u_2} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : dedekind_domain.prod_adic_completions 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.is_finite_adele = ∀ᶠ (v : is_dedekind_domain.height_one_spectrum R) in filter.cofinite , x v ∈ is_dedekind_domain.height_one_spectrum.adic_completion_integers K v

source

theorem dedekind_domain.prod_adic_completions.is_finite_adele.add {R : Type u_1} {K : Type u_2} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {x y : dedekind_domain.prod_adic_completions R K} (hx : x.is_finite_adele) (hy : y.is_finite_adele) :

(x + y).is_finite_adele

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

source

theorem dedekind_domain.prod_adic_completions.is_finite_adele.zero {R : Type u_1} {K : Type u_2} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

0.is_finite_adele

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

source

theorem dedekind_domain.prod_adic_completions.is_finite_adele.neg {R : Type u_1} {K : Type u_2} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {x : dedekind_domain.prod_adic_completions R K} (hx : x.is_finite_adele) :

(-x).is_finite_adele

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

source

theorem dedekind_domain.prod_adic_completions.is_finite_adele.mul {R : Type u_1} {K : Type u_2} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {x y : dedekind_domain.prod_adic_completions R K} (hx : x.is_finite_adele) (hy : y.is_finite_adele) :

(x * y).is_finite_adele

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

source

theorem dedekind_domain.prod_adic_completions.is_finite_adele.one {R : Type u_1} {K : Type u_2} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

1.is_finite_adele

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

source

def dedekind_domain.finite_adele_ring (R : Type u_1) (K : Type u_2) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

subring (dedekind_domain.prod_adic_completions R K)

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

dedekind_domain.finite_adele_ring R K = {carrier := {x : dedekind_domain.prod_adic_completions R K | x.is_finite_adele}, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, neg_mem' := _}

source

@[simp]

theorem dedekind_domain.mem_finite_adele_ring_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : dedekind_domain.prod_adic_completions R K) :

x ∈ dedekind_domain.finite_adele_ring R K ↔ x.is_finite_adele