mathlib documentation

ideles / ideles_number_field

The group of idèles of a number field #

We define the group of finite idèles and the group of idèles of a number field K, both of which are topological commutative groups.

We also prove that K* can be regarded as a subgroup of I_K_f and I_K and define the idèle class group of K as the quotient I_K/K*. We then show that the ideal class group of K is isomorphic to an explicit quotient of C_K as topological groups, by constructing a continuous surjective group homomorphism from C_K to the ideal class group Cl(K) of K and computing its kernel.

Main definitions #

number_field.I_K_f : The finite idèle group of the number field K.
number_field.I_K : The idèle group of the number field K.
number_field.C_K : The idèle class group of the number field K.
number_field.C_K.map_to_class_group : The natural group homomorphism from C_K to the Cl(K).

Main results #

number_field.C_K.map_to_class_group.surjective : The natural map C_K → Cl(K) is surjective.
number_field.C_K.map_to_class_group.continuous : The natural map C_K → Cl(K) is continuous.
number_field.C_K.map_to_class_group.mem_kernel_iff : We compute the kernel of C_K → Cl(K).

References #

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

Tags #

idèle group, number field

The idèle group of a number field #

We define the (finite) idèle group of a number field K, with its topological group structure. We define the idèle class group C_K of K and show that the ideal class group of K is isomorphic to an explicit quotient of C_K as topological groups.

def number_field.I_K_f (K : Type) [field K] [number_field K] :

Type

The finite idèle group of the number field K.

Equations

number_field.I_K_f K = (number_field.A_K_f K)ˣ

def number_field.I_K (K : Type) [field K] [number_field K] :

Type

The idèle group of the number field K.

Equations

number_field.I_K K = (number_field.A_K K)ˣ

@[protected, instance]

noncomputable def number_field.I_K_f.comm_group (K : Type) [field K] [number_field K] :

comm_group (number_field.I_K_f K)

Equations

number_field.I_K_f.comm_group K = units.comm_group

@[protected, instance]

noncomputable def number_field.I_K.comm_group (K : Type) [field K] [number_field K] :

comm_group (number_field.I_K K)

Equations

number_field.I_K.comm_group K = units.comm_group

@[protected, instance]

noncomputable def number_field.I_K_f.topological_space (K : Type) [field K] [number_field K] :

topological_space (number_field.I_K_f K)

Equations

number_field.I_K_f.topological_space K = finite_idele_group'.topological_space ↥(𝓞 K) K

@[protected, instance]

def number_field.I_K_f.topological_group (K : Type) [field K] [number_field K] :

topological_group (number_field.I_K_f K)

@[protected, instance]

noncomputable def number_field.I_K.topological_space (K : Type) [field K] [number_field K] :

topological_space (number_field.I_K K)

Equations

number_field.I_K.topological_space K = units.topological_space

@[protected, instance]

def number_field.I_K.topological_group (K : Type) [field K] [number_field K] :

topological_group (number_field.I_K K)

@[protected, instance]

noncomputable def number_field.I_K_f.inhabited (K : Type) [field K] [number_field K] :

inhabited (number_field.I_K_f K)

Equations

number_field.I_K_f.inhabited K = {default := 1}

@[protected, instance]

noncomputable def number_field.I_K.inhabited (K : Type) [field K] [number_field K] :

inhabited (number_field.I_K K)

Equations

number_field.I_K.inhabited K = {default := 1}

noncomputable def number_field.I_K.as_prod (K : Type) [field K] [number_field K] :

number_field.I_K K ≃* number_field.I_K_f K × (ℝ ⊗ K)ˣ

I_K is isomorphic to the product I_K_f × (ℝ ⊗[ℚ] K)*, as groups.

Equations

number_field.I_K.as_prod K = mul_equiv.prod_units

noncomputable def number_field.I_K.as_prod.homeo (K : Type) [field K] [number_field K] :

number_field.I_K K ≃ₜ number_field.I_K_f K × (ℝ ⊗ K)ˣ

I_K is homeomorphic to the product I_K_f × (ℝ ⊗[ℚ] K)*.

Equations

number_field.I_K.as_prod.homeo K = units.homeomorph.prod_units

theorem number_field.I_K.as_prod.continuous {K : Type} [field K] [number_field K] :

continuous (number_field.I_K.as_prod K).to_fun

theorem number_field.I_K.as_prod.continuous_inv {K : Type} [field K] [number_field K] :

continuous (number_field.I_K.as_prod K).inv_fun

noncomputable def number_field.I_K.mk {K : Type} [field K] [number_field K] (x : number_field.I_K_f K) (u : (ℝ ⊗ K)ˣ) :

number_field.I_K K

We construct an idèle of K given a finite idèle and a unit of ℝ ⊗[ℚ] K.

Equations

number_field.I_K.mk x u = (number_field.I_K.as_prod K).inv_fun (x, u)

noncomputable def number_field.I_K.fst (K : Type) [field K] [number_field K] :

number_field.I_K K →* number_field.I_K_f K

The projection from I_K to I_K_f, as a group homomorphism.

Equations

number_field.I_K.fst K = {to_fun := λ (x : number_field.I_K K), ((number_field.I_K.as_prod K).to_fun x).fst, map_one' := _, map_mul' := _}

theorem number_field.I_K.fst.surjective {K : Type} [field K] [number_field K] :

function.surjective ⇑(number_field.I_K.fst K)

The projection map I_K.fst is surjective.

theorem number_field.I_K.fst.continuous {K : Type} [field K] [number_field K] :

continuous ⇑(number_field.I_K.fst K)

The projection map I_K.fst is continuous.

theorem number_field.right_inv {K : Type} [field K] [number_field K] (x : Kˣ) :

(⇑(number_field.inj_K.ring_hom K) x.val) * ⇑(number_field.inj_K.ring_hom K) x.inv = 1

theorem number_field.left_inv {K : Type} [field K] [number_field K] (x : Kˣ) :

(⇑(number_field.inj_K.ring_hom K) x.inv) * ⇑(number_field.inj_K.ring_hom K) x.val = 1

noncomputable def number_field.inj_units_K_f (K : Type) [field K] [number_field K] :

Kˣ → number_field.I_K_f K

The map from K^* to I_K_f sending k to ((k)_v).

Equations

number_field.inj_units_K_f K = ⇑(units.map (number_field.inj_K_f.ring_hom K).to_monoid_hom)

noncomputable def number_field.inj_units_K (K : Type) [field K] [number_field K] :

Kˣ → number_field.I_K K

The map from K^* to I_K sending k to ((k)_v, 1 ⊗ k).

Equations

number_field.inj_units_K K = ⇑(units.map (number_field.inj_K.ring_hom K).to_monoid_hom)

@[simp]

theorem number_field.inj_units_K.map_one {K : Type} [field K] [number_field K] :

number_field.inj_units_K K 1 = 1

@[simp]

theorem number_field.inj_units_K.map_mul {K : Type} [field K] [number_field K] (x y : Kˣ) :

number_field.inj_units_K K (x * y) = (number_field.inj_units_K K x) * number_field.inj_units_K K y

noncomputable def number_field.inj_units_K.group_hom (K : Type) [field K] [number_field K] :

Kˣ →* number_field.I_K K

inj_units_K is a group homomorphism.

Equations

number_field.inj_units_K.group_hom K = {to_fun := number_field.inj_units_K K _inst_2, map_one' := _, map_mul' := _}

theorem number_field.inj_units_K.injective (K : Type) [field K] [number_field K] :

function.injective (number_field.inj_units_K K)

inj_units_K is injective.

def number_field.C_K (K : Type) [field K] [number_field K] :

Type

The idèle class group of K is the quotient of I_K by the group K* of principal idèles.

Equations

number_field.C_K K = (number_field.I_K K ⧸ (number_field.inj_units_K.group_hom K).range)

@[protected, instance]

noncomputable def number_field.C_K.comm_group (K : Type) [field K] [number_field K] :

comm_group (number_field.C_K K)

Equations

number_field.C_K.comm_group K = quotient_group.has_quotient.quotient.comm_group (number_field.inj_units_K.group_hom K).range

@[protected, instance]

noncomputable def number_field.C_K.topological_space (K : Type) [field K] [number_field K] :

topological_space (number_field.C_K K)

Equations

number_field.C_K.topological_space K = quotient.topological_space

@[protected, instance]

def number_field.C_K.topological_group (K : Type) [field K] [number_field K] :

topological_group (number_field.C_K K)

@[protected, instance]

noncomputable def number_field.C_K.inhabited (K : Type) [field K] [number_field K] :

inhabited (number_field.C_K K)

Equations

number_field.C_K.inhabited K = {default := 1}

noncomputable def number_field.v_comp_val (K : Type) [field K] [number_field K] (x : number_field.I_K K) (v : maximal_spectrum ↥(𝓞 K)) :

with_zero (multiplicative ℤ)

The v-adic absolute value of the vth component of the idèle x.

Equations

number_field.v_comp_val K x v = ⇑valued.v (x.val.fst.val v)

noncomputable def number_field.v_comp_inv (K : Type) [field K] [number_field K] (x : number_field.I_K K) (v : maximal_spectrum ↥(𝓞 K)) :

with_zero (multiplicative ℤ)

The v-adic absolute value of the inverse of the vth component of the idèle x.

Equations

number_field.v_comp_inv K x v = ⇑valued.v (x.inv.fst.val v)

theorem number_field.I_K_f.restricted_product (K : Type) [field K] [number_field K] (x : number_field.I_K_f K) :

({v : maximal_spectrum ↥(𝓞 K) | x.val.val v ∉ maximal_spectrum.adic_completion_integers K v} ∪ {v : maximal_spectrum ↥(𝓞 K) | 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 number_field.prod_val_inv_eq_one (K : Type) [field K] [number_field K] (x : number_field.I_K K) (v : maximal_spectrum ↥(𝓞 K)) :

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

theorem number_field.valuation.prod_val_inv_eq_one (K : Type) [field K] [number_field K] (x : number_field.I_K K) (v : maximal_spectrum ↥(𝓞 K)) :

(number_field.v_comp_val K x v) * number_field.v_comp_inv K x v = 1

theorem number_field.v_comp.ne_zero (K : Type) [field K] [number_field K] (x : number_field.I_K K) (v : maximal_spectrum ↥(𝓞 K)) :

x.val.fst.val v ≠ 0

theorem number_field.I_K.restricted_product (K : Type) [field K] [number_field K] (x : number_field.I_K K) :

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

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

theorem number_field.I_K.finite_exponents (K : Type) [field K] [number_field K] (x : number_field.I_K K) :

{v : maximal_spectrum ↥(𝓞 K) | number_field.v_comp_val K x v ≠ 1}.finite

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

noncomputable def number_field.I_K_f.map_to_fractional_ideals (K : Type) [field K] [number_field K] :

number_field.I_K_f K →* (fractional_ideal (↥(𝓞 K))⁰ K)ˣ

The natural map from I_K_f to the group of invertible fractional ideals of K, 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

number_field.I_K_f.map_to_fractional_ideals K = map_to_fractional_ideals ↥(𝓞 K) K

theorem number_field.I_K_f.map_to_fractional_ideals.surjective {K : Type} [field K] [number_field K] :

function.surjective ⇑(number_field.I_K_f.map_to_fractional_ideals K)

I_K_f.map_to_fractional_ideals is surjective.

theorem number_field.I_K_f.map_to_fractional_ideals.mem_kernel_iff {K : Type} [field K] [number_field K] (x : number_field.I_K_f K) :

⇑(number_field.I_K_f.map_to_fractional_ideals K) x = 1 ↔ ∀ (v : maximal_spectrum ↥(𝓞 K)), finite_idele.to_add_valuations ↥(𝓞 K) K x v = 0

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

theorem number_field.I_K_f.map_to_fractional_ideals.continuous {K : Type} [field K] [number_field K] :

continuous ⇑(number_field.I_K_f.map_to_fractional_ideals K)

I_K_f.map_to_fractional_ideals is continuous.

noncomputable def number_field.I_K.map_to_fractional_ideals (K : Type) [field K] [number_field K] :

number_field.I_K K →* (fractional_ideal (↥(𝓞 K))⁰ K)ˣ

The natural map from I_K to the group of invertible fractional ideals of K.

Equations

number_field.I_K.map_to_fractional_ideals K = (number_field.I_K_f.map_to_fractional_ideals K).comp (number_field.I_K.fst K)

theorem number_field.I_K.map_to_fractional_ideals.surjective {K : Type} [field K] [number_field K] :

function.surjective ⇑(number_field.I_K.map_to_fractional_ideals K)

I_K.map_to_fractional_ideals is surjective.

theorem number_field.I_K.map_to_fractional_ideals.mem_kernel_iff {K : Type} [field K] [number_field K] (x : number_field.I_K K) :

⇑(number_field.I_K.map_to_fractional_ideals K) x = 1 ↔ ∀ (v : maximal_spectrum ↥(𝓞 K)), finite_idele.to_add_valuations ↥(𝓞 K) K (⇑(number_field.I_K.fst K) x) v = 0

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

theorem number_field.I_K.map_to_fractional_ideals.continuous {K : Type} [field K] [number_field K] :

continuous ⇑(number_field.I_K.map_to_fractional_ideals K)

I_K.map_to_fractional_ideals is continuous.

noncomputable def number_field.I_K_f.map_to_class_group (K : Type) [field K] [number_field K] :

number_field.I_K_f K → class_group ↥(𝓞 K) K

The map from I_K_f to the ideal class group of K induced by I_K_f.map_to_fractional_ideals.

Equations

number_field.I_K_f.map_to_class_group K = λ (x : number_field.I_K_f K), quotient_group.mk (⇑(number_field.I_K_f.map_to_fractional_ideals K) x)

@[protected, instance]

def number_field.class_group.topological_space (K : Type) [field K] [number_field K] :

topological_space (class_group ↥(𝓞 K) K)

Equations

number_field.class_group.topological_space K = ⊥

@[protected, instance]

def number_field.class_group.topological_group (K : Type) [field K] [number_field K] :

topological_group (class_group ↥(𝓞 K) K)

theorem number_field.I_K_f.map_to_class_group.surjective {K : Type} [field K] [number_field K] :

function.surjective (number_field.I_K_f.map_to_class_group K)

theorem number_field.I_K_f.map_to_class_group.continuous {K : Type} [field K] [number_field K] :

continuous (number_field.I_K_f.map_to_class_group K)

noncomputable def number_field.I_K.map_to_class_group (K : Type) [field K] [number_field K] :

number_field.I_K K → class_group ↥(𝓞 K) K

The map from I_K to the ideal class group of K induced by I_K.map_to_fractional_ideals.

Equations

number_field.I_K.map_to_class_group K = λ (x : number_field.I_K K), ⇑(quotient_group.mk' (to_principal_ideal ↥(𝓞 K) K).range) (⇑(number_field.I_K.map_to_fractional_ideals K) x)

theorem number_field.I_K.map_to_class_group.surjective {K : Type} [field K] [number_field K] :

function.surjective (number_field.I_K.map_to_class_group K)

theorem number_field.I_K.map_to_class_group.continuous {K : Type} [field K] [number_field K] :

continuous (number_field.I_K.map_to_class_group K)

theorem number_field.I_K.map_to_class_group.map_one {K : Type} [field K] [number_field K] :

number_field.I_K.map_to_class_group K 1 = 1

theorem number_field.I_K.map_to_class_group.map_mul {K : Type} [field K] [number_field K] (x y : number_field.I_K K) :

number_field.I_K.map_to_class_group K (x * y) = (number_field.I_K.map_to_class_group K x) * number_field.I_K.map_to_class_group K y

noncomputable def number_field.I_K.monoid_hom_to_class_group {K : Type} [field K] [number_field K] :

number_field.I_K K →* class_group ↥(𝓞 K) K

The map from I_K to the ideal class group of K induced by I_K.map_to_fractional_ideals is a group homomorphism.

Equations

number_field.I_K.monoid_hom_to_class_group = {to_fun := number_field.I_K.map_to_class_group K _inst_2, map_one' := _, map_mul' := _}

theorem number_field.I_K_f.unit_image.mul_inv {K : Type} [field K] [number_field K] (k : Kˣ) :

(⇑(number_field.inj_K_f.ring_hom K) k.val) * ⇑(number_field.inj_K_f.ring_hom K) k.inv = 1

theorem number_field.I_K_f.unit_image.inv_mul {K : Type} [field K] [number_field K] (k : Kˣ) :

(⇑(number_field.inj_K_f.ring_hom K) k.inv) * ⇑(number_field.inj_K_f.ring_hom K) k.val = 1

theorem number_field.I_K_f.map_to_fractional_ideal.map_units {K : Type} [field K] [number_field K] (k : Kˣ) :

fractional_ideal.span_singleton (↥(𝓞 K))⁰ ↑k = ↑(⇑(number_field.I_K_f.map_to_fractional_ideals K) {val := ⇑(number_field.inj_K_f.ring_hom K) k.val, inv := ⇑(number_field.inj_K_f.ring_hom K) k.inv, val_inv := _, inv_val := _})

I_K_f.map_to_fractional_ideals sends the principal finite idèle (k)_v corresponding to k ∈ K* to the principal fractional ideal generated by k.

theorem number_field.I_K.map_to_fractional_ideals.map_units_K {K : Type} [field K] [number_field K] (k : Kˣ) :

fractional_ideal.span_singleton (↥(𝓞 K))⁰ ↑k = ↑(⇑(number_field.I_K.map_to_fractional_ideals K) (⇑(number_field.inj_units_K.group_hom K) k))

I_K.map_to_fractional_ideals sends the principal idèle (k)_v corresponding to k ∈ K* to the principal fractional ideal generated by k.

theorem number_field.I_K.map_to_class_group.map_units_K {K : Type} [field K] [number_field K] (k : Kˣ) :

number_field.I_K.map_to_class_group K (⇑(number_field.inj_units_K.group_hom K) k) = 1

The kernel of I_K.map_to_fractional_ideals contains the principal idèles (k)_v, for k ∈ K*.

def number_field.field.units.mk' {F : Type u_1} [field F] (k : F) (hk : k ≠ 0) :

Every nonzero element in a field is a unit.

Equations

number_field.field.units.mk' k hk = {val := k, inv := k⁻¹, val_inv := _, inv_val := _}

theorem number_field.I_K.map_to_fractional_ideals.apply {K : Type} [field K] [number_field K] (x : number_field.I_K K) :

↑(⇑(number_field.I_K.map_to_fractional_ideals K) x) = ∏ᶠ (v : maximal_spectrum ↥(𝓞 K)), ↑(v.as_ideal) ^ finite_idele.to_add_valuations ↥(𝓞 K) K (⇑(number_field.I_K.fst K) x) v

theorem number_field.I_K.map_to_class_group.valuation_mem_kernel {K : Type} [field K] [number_field K] (x : number_field.I_K K) (k : Kˣ) (v : maximal_spectrum ↥(𝓞 K)) (hkx : fractional_ideal.span_singleton (↥(𝓞 K))⁰ ↑k = ↑(⇑(number_field.I_K.map_to_fractional_ideals K) x)) :

⇑valued.v ((⇑(number_field.I_K.fst K) x).val.val v) = ⇑valued.v ↑(k.val)

If the image of x ∈ I_K under I_K.map_to_class_group is the principal fractional ideal generated by k ∈ K*, then for every maximal ideal v of the ring of integers of K, |x_v|_v = |k|_v.

theorem number_field.I_K.map_to_class_group.mem_kernel_iff {K : Type} [field K] [number_field K] (x : number_field.I_K K) :

number_field.I_K.map_to_class_group K x = 1 ↔ ∃ (k : K) (hk : k ≠ 0), ∀ (v : maximal_spectrum ↥(𝓞 K)), finite_idele.to_add_valuations ↥(𝓞 K) K (⇑(number_field.I_K.fst K) x) v = -with_zero.to_integer _

An element x ∈ I_K is in the kernel of C_K → Cl(K) if and only if there exist k ∈ K* and y ∈ I_K such that x = k*y and |y_v|_v = 1 for all v.

noncomputable def number_field.C_K.map_to_class_group (K : Type) [field K] [number_field K] :

number_field.C_K K →* class_group ↥(𝓞 K) K

The map C_K → Cl(K) induced by I_K.map_to_class_group.

Equations

number_field.C_K.map_to_class_group K = quotient_group.lift (number_field.inj_units_K.group_hom K).range number_field.I_K.monoid_hom_to_class_group _

theorem number_field.C_K.map_to_class_group.surjective (K : Type) [field K] [number_field K] :

function.surjective ⇑(number_field.C_K.map_to_class_group K)

The natural map C_K → Cl(K) is surjective.

theorem number_field.C_K.map_to_class_group.continuous (K : Type) [field K] [number_field K] :

continuous ⇑(number_field.C_K.map_to_class_group K)

The natural map C_K → Cl(K) is continuous.

theorem number_field.C_K.map_to_class_group.mem_kernel_iff (K : Type) [field K] [number_field K] (x : number_field.C_K K) :

⇑(number_field.C_K.map_to_class_group K) x = 1 ↔ ∃ (k : K) (hk : k ≠ 0), ∀ (v : maximal_spectrum ↥(𝓞 K)), finite_idele.to_add_valuations ↥(𝓞 K) K (⇑(number_field.I_K.fst K) (classical.some _)) v = -with_zero.to_integer _

An element x ∈ C_K is in the kernel of C_K → Cl(K) if and only if x comes from an idèle of the form k*y, with k ∈ K* and |y_v|_v = 1 for all v.