mathlib documentation

ideles / adeles_R

The finite adèle ring of a Dedekind domain #

Given a Dedekind domain R with field of fractions K and a maximal ideal v of R, we define the completion of K with respect to its v-adic valuation, denoted adic_completion, and its ring of integers, denoted adic_completion_integers.

We define the ring of finite adèles of a Dedekind domain. We provide two equivalent definitions of this ring (TODO: show that they are equivalent).

We show that there is an injective ring homomorphism from the field of fractions of a Dedekind domain of Krull dimension 1 to its finite adèle ring.

Main definitions #

adic_completion : the completion of K with respect to its v-adic valuation.
adic_completion_integers : the ring of integers of adic_completion.
R_hat : product of adic_completion_integers, where v runs over all maximal ideals of R.
K_hat : the product of adic_completion, where v runs over all maximal ideals of R.
finite_adele_ring' : The finite adèle ring of R, defined as the restricted product Π'_v adic_completion.
inj_K : The diagonal inclusion of K in finite_adele_ring' R K.
finite_adele_ring : The finite adèle ring of R, defined as the localization of R_hat at the submonoid R∖{0}.
finite_adele.hom : A ring homomorphism from finite_adele_ring R K to finite_adele_ring' R K.

Main results #

inj_K.ring_hom : inj_K is a ring homomorphism.
inj_K.injective : inj_K is injective for every Dedekind domain of Krull dimension 1.

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 empty.

References #

J.W.S. Cassels, A. Frölich, Algebraic Number Theory

Tags #

finite adèle ring, dedekind domain, completions

theorem mul_le_one₀ {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x y : α} (hx : x ≤ 1) (hy : y ≤ 1) :

x * y ≤ 1

noncomputable def force_noncomputable {α : Sort u_1} (a : α) :

α

Auxiliary definition to force a definition to be noncomputable. This is used to avoid timeouts or memory errors when Lean cannot decide whether a certain definition is computable. Author: Gabriel Ebner.

Equations

force_noncomputable a = function.const α a (classical.choice _)

@[simp]

theorem force_noncomputable_def {α : Sort u_1} (a : α) :

force_noncomputable a = a

Completions with respect to adic valuations #

Given a Dedekind domain R with field of fractions K and a maximal ideal v of R, we define the completion of K with respect to its v-adic valuation, denoted adic_completion,and its ring of integers, denoted adic_completion_integers.

We define R_hat (resp. K_hat) to be the product of adic_completion_integers (resp. adic_completion), where v runs over all maximal ideals of R.

noncomputable def maximal_spectrum.adic_valued {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

valued K (with_zero (multiplicative ℤ))

K as a valued field with the v-adic valuation.

Equations

v.adic_valued = {v := v.valuation}

theorem maximal_spectrum.adic_valued_def {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) {x : K} :

⇑valued.v x = v.valuation_def x

noncomputable def maximal_spectrum.ts' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

topological_space K

The topological space structure on K corresponding to the v-adic valuation.

Equations

v.ts' = valued.topological_space (with_zero (multiplicative ℤ))

theorem maximal_spectrum.tdr' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

topological_division_ring K

theorem maximal_spectrum.tr' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

topological_ring K

theorem maximal_spectrum.tg' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

topological_add_group K

noncomputable def maximal_spectrum.us' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

uniform_space K

The uniform space structure on K corresponding to the v-adic valuation.

Equations

v.us' = topological_add_group.to_uniform_space K

theorem maximal_spectrum.ug' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

uniform_add_group K

theorem maximal_spectrum.cf' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

completable_top_field K

theorem maximal_spectrum.ss {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

separated_space K

def maximal_spectrum.adic_completion {R : Type} (K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

Type

The completion of K with respect to its v-adic valuation.

Equations

maximal_spectrum.adic_completion K v = uniform_space.completion K

@[protected, instance]

noncomputable def maximal_spectrum.adic_completion.field {R : Type} (K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

field (maximal_spectrum.adic_completion K v)

Equations

maximal_spectrum.adic_completion.field K v = field_completion

@[protected, instance]

noncomputable def maximal_spectrum.adic_completion.inhabited {R : Type} (K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

inhabited (maximal_spectrum.adic_completion K v)

Equations

maximal_spectrum.adic_completion.inhabited K v = {default := 0}

@[protected, instance]

noncomputable def maximal_spectrum.valued_adic_completion {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

valued (maximal_spectrum.adic_completion K v) (with_zero (multiplicative ℤ))

Equations

v.valued_adic_completion = {v := valued.extension_valuation v.adic_valued}

theorem maximal_spectrum.valued_adic_completion_def {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) {x : maximal_spectrum.adic_completion K v} :

⇑valued.v x = valued.extension x

@[protected, instance]

noncomputable def maximal_spectrum.ts {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

topological_space (maximal_spectrum.adic_completion K v)

Equations

v.ts = valued.topological_space (with_zero (multiplicative ℤ))

@[protected, instance]

def maximal_spectrum.tdr {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

topological_division_ring (maximal_spectrum.adic_completion K v)

@[protected, instance]

def maximal_spectrum.tr {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

topological_ring (maximal_spectrum.adic_completion K v)

@[protected, instance]

def maximal_spectrum.tg {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

topological_add_group (maximal_spectrum.adic_completion K v)

@[protected, instance]

noncomputable def maximal_spectrum.us {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

uniform_space (maximal_spectrum.adic_completion K v)

Equations

v.us = uniform_space.completion.uniform_space K

@[protected, instance]

def maximal_spectrum.ug {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

uniform_add_group (maximal_spectrum.adic_completion K v)

@[protected, instance]

def maximal_spectrum.cs {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

complete_space (maximal_spectrum.adic_completion K v)

@[protected, instance]

noncomputable def maximal_spectrum.uniform_space.completion.has_lift_t {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

has_lift_t K (uniform_space.completion K)

Equations

maximal_spectrum.uniform_space.completion.has_lift_t v = infer_instance

@[protected, instance]

noncomputable def maximal_spectrum.adic_completion.has_lift_t {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

has_lift_t K (maximal_spectrum.adic_completion K v)

Equations

maximal_spectrum.adic_completion.has_lift_t v = maximal_spectrum.uniform_space.completion.has_lift_t v

noncomputable def maximal_spectrum.adic_completion_integers {R : Type} (K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

subring (maximal_spectrum.adic_completion K v)

The ring of integers of adic_completion.

Equations

maximal_spectrum.adic_completion_integers K v = valued.v.integer

def R_hat (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

Type

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

Equations

R_hat R K = Π (v : maximal_spectrum R), ↥(maximal_spectrum.adic_completion_integers K v)

@[protected, instance]

noncomputable def R_hat.comm_ring (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

comm_ring (R_hat R K)

Equations

R_hat.comm_ring R K = pi.comm_ring

@[protected, instance]

noncomputable def R_hat.topological_space (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_space (R_hat R K)

Equations

R_hat.topological_space R K = Pi.topological_space

@[protected, instance]

noncomputable def R_hat.inhabited (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inhabited (R_hat R K)

Equations

R_hat.inhabited R K = {default := λ (v : maximal_spectrum R), 0}

def K_hat (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

Type

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

Equations

K_hat R K = Π (v : maximal_spectrum R), maximal_spectrum.adic_completion K v

@[protected, instance]

noncomputable def K_hat.inhabited (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inhabited (K_hat R K)

Equations

K_hat.inhabited R K = {default := λ (v : maximal_spectrum R), 0}

@[protected, instance]

noncomputable def K_hat.comm_ring (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

comm_ring (K_hat R K)

Equations

K_hat.comm_ring R K = pi.comm_ring

@[protected, instance]

noncomputable def K_hat.ring (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

ring (K_hat R K)

Equations

K_hat.ring R K = infer_instance

@[protected, instance]

noncomputable def K_hat.topological_space (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_space (K_hat R K)

Equations

K_hat.topological_space R K = Pi.topological_space

@[protected, instance]

def tr_hat (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_ring (Π (v : maximal_spectrum R), maximal_spectrum.adic_completion K v)

@[protected, instance]

def K_hat.topological_ring (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_ring (K_hat R K)

theorem adic_completion.is_integer (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) (x : maximal_spectrum.adic_completion K v) :

x ∈ maximal_spectrum.adic_completion_integers K v ↔ ⇑valued.v x ≤ 1

noncomputable def inj_adic_completion_integers' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

R → maximal_spectrum.adic_completion K v

The natural inclusion of R in adic_completion.

Equations

inj_adic_completion_integers' R K v = λ (r : R), ↑(⇑(algebra_map R K) r)

noncomputable def inj_adic_completion_integers (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

R → ↥(maximal_spectrum.adic_completion_integers K v)

The natural inclusion of R in adic_completion_integers.

Equations

inj_adic_completion_integers R K v = λ (r : R), ⟨↑(⇑(algebra_map R K) r), _⟩

noncomputable def inj_R (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

R → R_hat R K

The diagonal inclusion r ↦ (r)_v of R in R_hat.

Equations

inj_R R K = λ (r : R) (v : maximal_spectrum R), inj_adic_completion_integers R K v r

theorem uniform_space.completion.coe_inj {α : Type u_1} [uniform_space α] [separated_space α] :

function.injective coe

theorem inj_adic_completion_integers.injective (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

function.injective (inj_adic_completion_integers R K v)

theorem inj_adic_completion_integers.map_one (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

inj_adic_completion_integers R K v 1 = 1

theorem inj_R.map_one (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inj_R R K 1 = 1

theorem inj_adic_completion_integers.map_mul (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) (x y : R) :

inj_adic_completion_integers R K v (x * y) = (inj_adic_completion_integers R K v x) * inj_adic_completion_integers R K v y

theorem inj_R.map_mul (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : R) :

inj_R R K (x * y) = (inj_R R K x) * inj_R R K y

def group_hom_prod (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

R_hat R K →+ K_hat R K

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

Equations

group_hom_prod R K = {to_fun := λ (x : R_hat R K) (v : maximal_spectrum R), ↑(x v), map_zero' := _, map_add' := _}

def hom_prod (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

R_hat R K →+* K_hat R K

The inclusion of R_hat in K_hat is a ring homomorphism.

Equations

hom_prod R K = {to_fun := λ (x : R_hat R K) (v : maximal_spectrum R), ↑(x v), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

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 and give it a topology that makes it into a topological ring.

def restricted (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

K_hat R K → Prop

A tuple (x_v)_v is in the restricted product of the adic_completion with respect to adic_completion_integers if for all but finitely many v, x_v ∈ adic_completion_integers.

Equations

restricted R K = λ (x : K_hat R K), ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, x v ∈ maximal_spectrum.adic_completion_integers K v

def finite_adele_ring' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

Type

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

finite_adele_ring' R K = {x // ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, x v ∈ maximal_spectrum.adic_completion_integers K v}

def coe' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

finite_adele_ring' R K → K_hat R K

The coercion map from finite_adele_ring' R K to K_hat R K.

Equations

coe' R K = λ (x : finite_adele_ring' R K), x.val

@[protected, instance]

noncomputable def has_coe' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

has_coe (finite_adele_ring' R K) (K_hat R K)

Equations

has_coe' R K = {coe := coe' R K _inst_6}

@[protected, instance]

noncomputable def has_lift_t' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

has_lift_t (finite_adele_ring' R K) (K_hat R K)

Equations

has_lift_t' R K = {lift := coe' R K _inst_6}

theorem restr_add (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring' R K) :

∀ᶠ (v : maximal_spectrum R) in filter.cofinite, (x.val + y.val) v ∈ maximal_spectrum.adic_completion_integers K v

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

noncomputable def add' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring' R K) :

finite_adele_ring' R K

Addition on the finite adèle. ring.

Equations

add' R K x y = ⟨x.val + y.val, _⟩

theorem restr_zero (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

∀ᶠ (v : maximal_spectrum R) in filter.cofinite, 0 ∈ maximal_spectrum.adic_completion_integers K v

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

theorem restr_neg (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : finite_adele_ring' R K) :

∀ᶠ (v : maximal_spectrum R) in filter.cofinite, -x.val v ∈ maximal_spectrum.adic_completion_integers K v

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

noncomputable def neg' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : finite_adele_ring' R K) :

finite_adele_ring' R K

Negation on the finite adèle ring.

Equations

neg' R K x = ⟨-x.val, _⟩

theorem restr_mul (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring' R K) :

∀ᶠ (v : maximal_spectrum R) in filter.cofinite, ((x.val) * y.val) v ∈ maximal_spectrum.adic_completion_integers K v

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

noncomputable def mul' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring' R K) :

finite_adele_ring' R K

Multiplication on the finite adèle ring.

Equations

mul' R K x y = ⟨(x.val) * y.val, _⟩

theorem restr_one (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

∀ᶠ (v : maximal_spectrum R) in filter.cofinite, 1 ∈ maximal_spectrum.adic_completion_integers K v

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

@[protected, instance]

noncomputable def finite_adele_ring'.add_comm_group (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

add_comm_group (finite_adele_ring' R K)

finite_adele_ring' R K is a commutative additive group.

Equations

finite_adele_ring'.add_comm_group R K = {add := add' R K _inst_6, add_assoc := _, zero := ⟨0, _⟩, zero_add := _, add_zero := _, nsmul := add_group.nsmul._default ⟨0, _⟩ (add' R K) _ _, nsmul_zero' := _, nsmul_succ' := _, neg := λ (x : finite_adele_ring' R K), ⟨-x.val, _⟩, sub := add_group.sub._default (add' R K) _ ⟨0, _⟩ _ _ (add_group.nsmul._default ⟨0, _⟩ (add' R K) _ _) _ _ (λ (x : finite_adele_ring' R K), ⟨-x.val, _⟩), sub_eq_add_neg := _, zsmul := add_group.zsmul._default (add' R K) _ ⟨0, _⟩ _ _ (add_group.nsmul._default ⟨0, _⟩ (add' R K) _ _) _ _ (λ (x : finite_adele_ring' R K), ⟨-x.val, _⟩), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

@[protected, instance]

noncomputable def finite_adele_ring'.comm_ring (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

comm_ring (finite_adele_ring' R K)

finite_adele_ring' R K is a commutative ring.

Equations

finite_adele_ring'.comm_ring R K = {add := add_comm_group.add (finite_adele_ring'.add_comm_group R K), add_assoc := _, zero := add_comm_group.zero (finite_adele_ring'.add_comm_group R K), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (finite_adele_ring'.add_comm_group R K), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (finite_adele_ring'.add_comm_group R K), sub := add_comm_group.sub (finite_adele_ring'.add_comm_group R K), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (finite_adele_ring'.add_comm_group R K), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul' R K _inst_6, mul_assoc := _, one := ⟨1, _⟩, one_mul := _, mul_one := _, npow := ring.npow._default ⟨1, _⟩ (mul' R K) _ _, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[norm_cast]

theorem finite_adele_ring'.coe_add (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring' R K) :

↑(x + y) = ↑x + ↑y

@[norm_cast]

theorem finite_adele_ring'.coe_zero (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

↑0 = 0

@[norm_cast]

theorem finite_adele_ring'.coe_neg (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : finite_adele_ring' R K) :

@[norm_cast]

theorem finite_adele_ring'.coe_mul (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring' R K) :

↑x * y = (↑x) * ↑y

@[norm_cast]

theorem finite_adele_ring'.coe_one (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

↑1 = 1

@[protected, instance]

noncomputable def finite_adele_ring'.inhabited (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inhabited (finite_adele_ring' R K)

Equations

finite_adele_ring'.inhabited R K = {default := ⟨0, _⟩}

theorem adic_completion.is_open_adic_completion_integers (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (v : maximal_spectrum R) :

is_open ↑(maximal_spectrum.adic_completion_integers K v)

The ring of integers adic_completion_integers is an open subset of adic_completion.

def finite_adele_ring'.generating_set (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

set (set (finite_adele_ring' R K))

A generating set for the topology on the finite adèle ring of R consists on products ∏_v U_v of open sets such that U_v = adic_completion_integers for all but finitely many maximal ideals v.

Equations

finite_adele_ring'.generating_set R K = {U : set (finite_adele_ring' R K) | ∃ (V : Π (v : maximal_spectrum R), set (maximal_spectrum.adic_completion K v)), (∀ (x : finite_adele_ring' R K), x ∈ U ↔ ∀ (v : maximal_spectrum R), x.val v ∈ V v) ∧ (∀ (v : maximal_spectrum R), is_open (V v)) ∧ ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, V v = ↑(maximal_spectrum.adic_completion_integers K v)}

@[protected, instance]

def finite_adele_ring'.topological_space (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_space (finite_adele_ring' R K)

The topology on the finite adèle ring of R.

Equations

finite_adele_ring'.topological_space R K = topological_space.generate_from (finite_adele_ring'.generating_set R K)

theorem finite_adele_ring'.continuous_add (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

continuous (λ (p : finite_adele_ring' R K × finite_adele_ring' R K), p.fst + p.snd)

Addition on the finite adèle ring of R is continuous.

theorem finite_adele_ring'.continuous_mul (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

continuous (λ (p : finite_adele_ring' R K × finite_adele_ring' R K), (p.fst) * p.snd)

Multiplication on the finite adèle ring of R is continuous.

@[protected, instance]

def finite_adele_ring'.has_continuous_mul (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

has_continuous_mul (finite_adele_ring' R K)

@[protected, instance]

def finite_adele_ring'.topological_ring (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_ring (finite_adele_ring' R K)

The finite adèle ring of R is a topological ring.

theorem finite_adele_ring'.is_open_integer_subring (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

is_open {x : finite_adele_ring' R K | ∀ (v : maximal_spectrum R), x.val v ∈ maximal_spectrum.adic_completion_integers K v}

The product ∏_v adic_completion_integers is an open subset of the finite adèle ring of R.

theorem finite_adele_ring'.is_open_integer_subring_opp (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

is_open {x : (finite_adele_ring' R K)ᵐᵒᵖ | ∀ (v : maximal_spectrum R), (mul_opposite.unop x).val v ∈ maximal_spectrum.adic_completion_integers K v}

@[protected, instance]

noncomputable def subtype.comm_ring (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

comm_ring {x // ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, x v ∈ maximal_spectrum.adic_completion_integers K v}

Equations

subtype.comm_ring R K = finite_adele_ring'.comm_ring R K

theorem mul_apply (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring' R K) :

⟨(x.val) * y.val, _⟩ = x * y

theorem mul_apply_val (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring' R K) :

(x.val) * y.val = (x * y).val

@[simp]

theorem one_def (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

⟨1, _⟩ = 1

@[simp]

theorem zero_def (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

⟨0, _⟩ = 0

theorem inj_K_image (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : K) :

{v : maximal_spectrum R | ↑x ∉ maximal_spectrum.adic_completion_integers K v}.finite

For any x ∈ K, the tuple (x)_v is a finite adèle.

@[simp]

theorem inj_K_coe (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (ᾰ : K) (v : maximal_spectrum R) :

↑(inj_K R K ᾰ) v = ↑ᾰ

noncomputable def inj_K (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

K → finite_adele_ring' R K

The diagonal inclusion k ↦ (k)_v of K into the finite adèle ring of R.

Equations

inj_K R K = λ (x : K), ⟨λ (v : maximal_spectrum R), ↑x, _⟩

theorem inj_K_apply (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (k : K) :

inj_K R K k = ⟨λ (v : maximal_spectrum R), ↑k, _⟩

@[simp]

theorem inj_K.map_zero (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inj_K R K 0 = 0

@[simp]

theorem inj_K.map_add (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : K) :

inj_K R K (x + y) = inj_K R K x + inj_K R K y

@[simp]

theorem inj_K.map_one (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inj_K R K 1 = 1

@[simp]

theorem inj_K.map_mul (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : K) :

inj_K R K (x * y) = (inj_K R K x) * inj_K R K y

noncomputable def inj_K.add_group_hom (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

K →+ finite_adele_ring' R K

The map inj_K is an additive group homomorphism.

Equations

inj_K.add_group_hom R K = {to_fun := inj_K R K _inst_6, map_zero' := _, map_add' := _}

noncomputable def inj_K.ring_hom (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

K →+* finite_adele_ring' R K

The map inj_K is a ring homomorphism.

Equations

inj_K.ring_hom R K = {to_fun := inj_K R K _inst_6, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

theorem inj_K.ring_hom_apply (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {k : K} :

⇑(inj_K.ring_hom R K) k = inj_K R K k

theorem inj_K.injective (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] [inh : nonempty (maximal_spectrum R)] :

function.injective ⇑(inj_K.ring_hom R K)

If maximal_spectrum R is nonempty, then inj_K is injective. Note that the nonemptiness hypothesis is satisfied for every Dedekind domain that is not a field.

Alternative definition of the finite adèle ring #

We can also define the finite adèle ring of R as the localization of R_hat at R∖{0}. We denote this definition by finite_adele_ring and construct a ring homomorphism from finite_adele_ring R to finite_adele_ring' R. TODO: show that this homomorphism is in fact an isomorphism of topological rings.

def diag_R (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

submonoid (R_hat R K)

R∖{0} is a submonoid of R_hat R K, via the inclusion r ↦ (r)_v.

Equations

diag_R R K = {carrier := inj_R R K '' {0}.compl, mul_mem' := _, one_mem' := _}

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

Type

The finite adèle ring of R as the localization of R_hat at R∖{0}.

Equations

finite_adele_ring R K = localization (diag_R R K)

@[protected, instance]

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

comm_ring (finite_adele_ring R K)

Equations

finite_adele_ring.comm_ring R K = localization.comm_ring

@[protected, instance]

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

algebra (R_hat R K) (finite_adele_ring R K)

Equations

finite_adele_ring.algebra R K = localization.algebra

@[protected, instance]

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

is_localization (diag_R R K) (finite_adele_ring R K)

@[protected, instance]

noncomputable def finite_adele_ring.topological_space (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

topological_space (finite_adele_ring R K)

Equations

finite_adele_ring.topological_space R K = localization.topological_space

@[protected, instance]

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

topological_ring (finite_adele_ring R K)

@[protected, instance]

noncomputable def finite_adele_ring.inhabited (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

inhabited (finite_adele_ring R K)

Equations

finite_adele_ring.inhabited R K = localization.inhabited (diag_R R K)

theorem preimage_diag_R (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : ↥(diag_R R K)) :

∃ (r : R), r ≠ 0 ∧ inj_R R K r = ↑x

theorem hom_prod_diag_unit (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : ↥(diag_R R K)) :

is_unit (⇑(hom_prod R K) ↑x)

For every r ∈ R, (r)_v is a unit of K_hat R K.

noncomputable def map_to_K_hat (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : finite_adele_ring R K) :

The map from finite_adele_ring R K to K_hat R K induced by hom_prod.

Equations

map_to_K_hat R K x = ⇑(is_localization.lift _) x

theorem restricted_image (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x : finite_adele_ring R K) :

{v : maximal_spectrum R | map_to_K_hat R K x v ∉ maximal_spectrum.adic_completion_integers K v}.finite

The image of map_to_K_hat R K is contained in finite_adele_ring' R K.

theorem map_to_K_hat.map_one (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

map_to_K_hat R K 1 = 1

theorem map_to_K_hat.map_mul (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring R K) :

map_to_K_hat R K (x * y) = (map_to_K_hat R K x) * map_to_K_hat R K y

theorem map_to_K_hat.map_add (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (x y : finite_adele_ring R K) :

map_to_K_hat R K (x + y) = map_to_K_hat R K x + map_to_K_hat R K y

theorem map_to_K_hat.map_zero (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

map_to_K_hat R K 0 = 0

noncomputable def finite_adele.hom (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] :

finite_adele_ring R K →+* finite_adele_ring' R K

map_to_K_hat is a ring homomorphism between our two definitions of finite adèle ring.

Equations

finite_adele.hom R K = {to_fun := λ (x : finite_adele_ring R K), ⟨map_to_K_hat R K x, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}