mathlib documentation

ideles / ideles_R

The finite idèle group of a Dedekind domain #

We define the finite idèle group of a Dedekind domain R and show that if R has Krull dimension 1, then there is an injective group homomorphism from the units of the field of fractions of R to its finite adèle ring.

We prove that there is a continuous surjective group homomorphism from the finite idèle group of R to the group of invertible fractional ideals of R and compute the kernel of this map.

Main definitions #

finite_idele_group' : The finite idèle group of R, defined as unit group of A_R_f R.
inj_units_K : The diagonal inclusion of K* in finite_idele_group' R K.
map_to_fractional_ideals : The group homomorphism from finite_idele_group' R K to the group of Fr(R) of invertible fractional_ideals of R sending a finite idèle x to the product ∏_v v^(val_v(x_v)), where val_v denotes the additive v-adic valuation.

Main results #

inj_units_K.group_hom : inj_units_K is a group homomorphism.
inj_units_K.injective : inj_units_K is injective for every Dedekind domain of Krull dimension 1.
map_to_fractional_ideals.surjective : map_to_fractional_ideals is surjective.
map_to_fractional_ideals.continuous : map_to_fractional_ideals is continuous when the group of fractional ideals is given the discrete topology.
map_to_fractional_ideals.mem_kernel_iff : A finite idèle x is in the kernel of map_to_fractional_ideals if and only if |x_v|_v = 1 for all v.

Implementation notes #

As in adeles_R, we are only interested on Dedekind domains of Krull dimension 1.

References #

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

Tags #

finite idèle group, dedekind domain, fractional ideal

The finite idèle group of a Dedekind domain #

def finite_idele_group' (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 idèle group of R is the unit group of its finite adèle ring.

Equations

finite_idele_group' R K = (finite_adele_ring' R K)ˣ

@[protected, instance]

noncomputable def finite_idele_group'.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_idele_group' R K)

Equations

finite_idele_group'.topological_space R K = units.topological_space

@[protected, instance]

noncomputable def finite_idele_group'.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] :

comm_group (finite_idele_group' R K)

Equations

finite_idele_group'.comm_group R K = units.comm_group

@[protected, instance]

noncomputable def finite_idele_group'.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_idele_group' R K)

Equations

finite_idele_group'.inhabited R K = {default := 1}

@[protected, instance]

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

topological_group (finite_idele_group' R K)

@[protected, instance]

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

uniform_space (finite_idele_group' R K)

Equations

finite_idele_group'.uniform_space R K = topological_group.to_uniform_space (finite_idele_group' R K)

@[protected, instance]

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

uniform_group (finite_idele_group' R K)

theorem right_inv (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ˣ) :

(inj_K R K x.val) * inj_K R K x.inv = 1

theorem left_inv (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ˣ) :

(inj_K R K x.inv) * inj_K R K x.val = 1

noncomputable def inj_units_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_idele_group' R K

The diagonal inclusion k ↦ (k)_v of K* into the finite idèle group of R.

Equations

inj_units_K R K = λ (x : Kˣ), {val := inj_K R K x.val, inv := inj_K R K x.inv, val_inv := _, inv_val := _}

@[simp]

theorem inj_units_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_units_K R K 1 = 1

@[simp]

theorem inj_units_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_units_K R K (x * y) = (inj_units_K R K x) * inj_units_K R K y

noncomputable def inj_units_K.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_idele_group' R K

The map inj_units_K is a group homomorphism.

Equations

inj_units_K.group_hom R K = {to_fun := inj_units_K R K _inst_6, map_one' := _, map_mul' := _}

theorem inj_units_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_units_K.group_hom R K)

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

theorem prod_val_inv_eq_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) (x : finite_idele_group' R K) :

(x.val.val v) * x.inv.val v = 1

theorem v_comp.ne_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) (x : finite_idele_group' R K) :

x.val.val v ≠ 0

theorem valuation_val_inv (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 : finite_idele_group' R K) :

(⇑valued.v (x.val.val v)) * ⇑valued.v (x.inv.val v) = 1

theorem valuation_inv (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 : finite_idele_group' R K) :

⇑valued.v (x.inv.val v) = (⇑valued.v (x.val.val v))⁻¹

theorem restricted_product (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_idele_group' R K) :

({v : maximal_spectrum R | x.val.val v ∉ maximal_spectrum.adic_completion_integers K v} ∪ {v : maximal_spectrum R | x.inv.val v ∉ maximal_spectrum.adic_completion_integers K v}).finite

For any finite idèle x, there are finitely many maximal ideals v of R for which x_v ∉ R_v or x⁻¹_v ∉ R_v.

theorem finite_exponents (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_idele_group' R K) :

{v : maximal_spectrum R | ⇑valued.v (x.val.val v) ≠ 1}.finite

For any finite idèle x, there are finitely many maximal ideals v of R for which |x_v|_v ≠ 1.

theorem units.valuation_ne_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) {k : K} (hk : k ≠ 0) :

⇑valued.v ↑k ≠ 0

For any k ∈ K* and any maximal ideal v of R, the valuation |k|_v is nonzero.

noncomputable def with_zero.to_integer {x : with_zero (multiplicative ℤ)} (hx : x ≠ 0) :

The integer number corresponding to a nonzero x in with_zero (multiplicative ℤ).

Equations

with_zero.to_integer hx = ⇑multiplicative.to_add (classical.some _)

noncomputable def finite_idele.to_add_valuations (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_idele_group' R K) (v : maximal_spectrum R) :

Given a finite idèle x, for each maximal ideal v of R we obtain an integer that represents the additive v-adic valuation of the component x_v of x.

Equations

finite_idele.to_add_valuations R K x = λ (v : maximal_spectrum R), -with_zero.to_integer _

theorem finite_idele.to_add_valuations.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] :

finite_idele.to_add_valuations R K 1 = λ (v : maximal_spectrum R), 0

theorem finite_idele.to_add_valuations.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_idele_group' R K) :

finite_idele.to_add_valuations R K (x * y) = finite_idele.to_add_valuations R K x + finite_idele.to_add_valuations R K y

theorem finite_add_support (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_idele_group' R K) :

∀ᶠ (v : maximal_spectrum R) in filter.cofinite, finite_idele.to_add_valuations R K x v = 0

For any finite idèle x, there are finitely many maximal ideals v of R for which the additive v-adic valuation of x_v is nonzero.

theorem finite_support (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_idele_group' R K) :

(function.mul_support (λ (v : maximal_spectrum R), ↑(v.as_ideal) ^ finite_idele.to_add_valuations R K x v)).finite

For any finite idèle x, there are finitely many maximal ideals v of R for which v^(finite_idele.to_add_valuations R K x v) is not the fractional ideal (1).

theorem finite_support' (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_idele_group' R K) :

(function.mul_support (λ (v : maximal_spectrum R), ↑(v.as_ideal) ^ -finite_idele.to_add_valuations R K x v)).finite

For any finite idèle x, there are finitely many maximal ideals v of R for which v^-(finite_idele.to_add_valuations R K x v) is not the fractional ideal (1).

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

finite_idele_group' R K → fractional_ideal R⁰ K

The map from finite_idele_group' R K to the fractional_ideals of R sending a finite idèle x to the product ∏_v v^(val_v(x_v)), where val_v denotes the additive v-adic valuation.

Equations

map_to_fractional_ideals.val R K = λ (x : finite_idele_group' R K), ∏ᶠ (v : maximal_spectrum R), ↑(v.as_ideal) ^ finite_idele.to_add_valuations R K x v

noncomputable def map_to_fractional_ideals.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] :

finite_idele_group' R K →* fractional_ideal R⁰ K

The group homomorphism from finite_idele_group' R K to the fractional_ideals of R sending a finite idèle x to the product ∏_v v^(val_v(x_v))

Equations

map_to_fractional_ideals.group_hom R K = {to_fun := map_to_fractional_ideals.val R K _inst_6, map_one' := _, map_mul' := _}

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

finite_idele_group' R K → fractional_ideal R⁰ K

The map from finite_idele_group' R K to the fractional_ideals of R sending a finite idèle x to the product ∏_v v^-(val_v(x_v)), where val_v denotes the additive v-adic valuation.

Equations

map_to_fractional_ideals.inv R K = λ (x : finite_idele_group' R K), ∏ᶠ (v : maximal_spectrum R), ↑(v.as_ideal) ^ -finite_idele.to_add_valuations R K x v

theorem finite_idele.to_add_valuations.mul_inv (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_idele_group' R K) :

(map_to_fractional_ideals.val R K x) * map_to_fractional_ideals.inv R K x = 1

theorem finite_idele.to_add_valuations.inv_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 : finite_idele_group' R K) :

(map_to_fractional_ideals.inv R K x) * map_to_fractional_ideals.val R K x = 1

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

finite_idele_group' R K → (fractional_ideal R⁰ K)ˣ

The map from finite_idele_group' R K to the units of the fractional_ideals of R sending a finite idèle x to the product ∏_v v^(val_v(x_v)), where val_v denotes the additive v-adic valuation.

Equations

map_to_fractional_ideals.def R K = λ (x : finite_idele_group' R K), {val := map_to_fractional_ideals.val R K x, inv := map_to_fractional_ideals.inv R K x, val_inv := _, inv_val := _}

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

finite_idele_group' R K →* (fractional_ideal R⁰ K)ˣ

map_to_fractional_ideals.def is a group homomorphism.

Equations

map_to_fractional_ideals R K = {to_fun := map_to_fractional_ideals.def R K _inst_6, map_one' := _, map_mul' := _}

theorem val_property {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {a : Π (v : maximal_spectrum R), maximal_spectrum.adic_completion K v} (ha : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, ⇑valued.v (a v) = 1) :

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

theorem inv_property {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {a : Π (v : maximal_spectrum R), maximal_spectrum.adic_completion K v} (ha : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, ⇑valued.v (a v) = 1) :

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

theorem right_inv' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {a : Π (v : maximal_spectrum R), maximal_spectrum.adic_completion K v} (ha : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, ⇑valued.v (a v) = 1) (h_ne_zero : ∀ (v : maximal_spectrum R), a v ≠ 0) :

⟨a, _⟩ * ⟨λ (v : maximal_spectrum R), (a v)⁻¹, _⟩ = 1

theorem left_inv' {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {a : Π (v : maximal_spectrum R), maximal_spectrum.adic_completion K v} (ha : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, ⇑valued.v (a v) = 1) (h_ne_zero : ∀ (v : maximal_spectrum R), a v ≠ 0) :

⟨λ (v : maximal_spectrum R), (a v)⁻¹, _⟩ * ⟨a, _⟩ = 1

noncomputable def idele.mk {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] (a : Π (v : maximal_spectrum R), maximal_spectrum.adic_completion K v) (ha : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, ⇑valued.v (a v) = 1) (h_ne_zero : ∀ (v : maximal_spectrum R), a v ≠ 0) :

finite_idele_group' R K

If a = (a_v)_v ∈ ∏_v K_v is such that |a_v|_v ≠ 1 for all but finitely many v and a_v ≠ 0 for all v, then a is a finite idèle of R.

Equations

idele.mk a ha h_ne_zero = {val := ⟨a, _⟩, inv := ⟨λ (v : maximal_spectrum R), (a v)⁻¹, _⟩, val_inv := _, inv_val := _}

theorem map_to_fractional_ideals.inv_eq_inv {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_idele_group' R K) (I : (fractional_ideal R⁰ K)ˣ) (hxI : map_to_fractional_ideals.val R K x = I.val) :

map_to_fractional_ideals.inv R K x = I.inv

noncomputable def pi.unif (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) :

maximal_spectrum.adic_completion K v

A finite idèle (pi_v)_v, where each pi_v is a uniformizer for the v-adic valuation.

Equations

pi.unif R K = λ (v : maximal_spectrum R), ↑(classical.some _)

theorem pi.unif.ne_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) :

pi.unif R K v ≠ 0

theorem idele.mk'.val {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {exps : maximal_spectrum R → ℤ} (h_exps : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, exps v = 0) :

∀ᶠ (v : maximal_spectrum R) in filter.cofinite, pi.unif R K v ^ exps v ∈ maximal_spectrum.adic_completion_integers K v

theorem idele.mk'.inv {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {exps : maximal_spectrum R → ℤ} (h_exps : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, exps v = 0) :

∀ᶠ (v : maximal_spectrum R) in filter.cofinite, pi.unif R K v ^ -exps v ∈ maximal_spectrum.adic_completion_integers K v

theorem idele.mk'.mul_inv {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {exps : maximal_spectrum R → ℤ} (h_exps : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, exps v = 0) :

⟨λ (v : maximal_spectrum R), pi.unif R K v ^ exps v, _⟩ * ⟨λ (v : maximal_spectrum R), pi.unif R K v ^ -exps v, _⟩ = 1

theorem idele.mk'.inv_mul {R K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {exps : maximal_spectrum R → ℤ} (h_exps : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, exps v = 0) :

⟨λ (v : maximal_spectrum R), pi.unif R K v ^ -exps v, _⟩ * ⟨λ (v : maximal_spectrum R), pi.unif R K v ^ exps v, _⟩ = 1

noncomputable def idele.mk' (R K : Type) [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K] [algebra R K] [is_fraction_ring R K] {exps : maximal_spectrum R → ℤ} (h_exps : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, exps v = 0) :

finite_idele_group' R K

Given a collection exps of integers indexed by the maximal ideals v of R, of which only finitely many are allowed to be nonzero, (pi_v^(exps v))_v is a finite idèle of R.

Equations

idele.mk' R K h_exps = {val := ⟨λ (v : maximal_spectrum R), pi.unif R K v ^ exps v, _⟩, inv := ⟨λ (v : maximal_spectrum R), pi.unif R K v ^ -exps v, _⟩, val_inv := _, inv_val := _}

theorem idele.mk'.valuation_ne_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) {exps : maximal_spectrum R → ℤ} (h_exps : ∀ᶠ (v : maximal_spectrum R) in filter.cofinite, exps v = 0) :

⇑valued.v ((idele.mk' R K h_exps).val.val v) ≠ 0

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

function.surjective ⇑(map_to_fractional_ideals R K)

map_to_fractional_ideals is surjective.

theorem map_to_fractional_ideals.mem_kernel_iff {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_idele_group' R K) :

⇑(map_to_fractional_ideals R K) x = 1 ↔ ∀ (v : maximal_spectrum R), finite_idele.to_add_valuations R K x v = 0

A finite idèle x is in the kernel of map_to_fractional_ideals if and only if |x_v|_v = 1 for all v.

theorem finite_idele.to_add_valuations.comp_eq_zero_iff (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 : finite_idele_group' R K) :

finite_idele.to_add_valuations R K x v = 0 ↔ ⇑valued.v (x.val.val v) = 1

The additive v-adic valuation of x_v equals 0 if and only if |x_v|_v = 1

theorem finite_idele.valuation_eq_one_iff (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 : finite_idele_group' R K) :

⇑valued.v (x.val.val v) = 1 ↔ x.val.val v ∈ maximal_spectrum.adic_completion_integers K v ∧ x⁻¹.val.val v ∈ maximal_spectrum.adic_completion_integers K v

|x_v|_v = 1 if and only if both x_v and x⁻¹_v are in R_v.

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

continuous ⇑(map_to_fractional_ideals R K)

map_to_fractional_ideals is continuous, where the codomain is given the discrete topology.