mathlib documentation

ideles / adeles_number_field

The ring of adèles of a number field #

We define the ring of finite adèles and the ring of adèles of a number field, both of which are topological commutative rings.

Main definitions #

number_field.A_K_f : The finite adèle ring of the number field K.
number_field.A_K : The adèle ring of the number field K.
number_field.inj_K_f : The map from K to A_K_f K sending k ∈ K ↦ (k)_v
number_field.inj_K : The map from K to A_K K sending k ∈ K ↦ ((k)_v, 1 ⊗ k).

Main results #

number_field.inj_K_f.injective : The map inj_K_f is injective.
number_field.inj_K_f.ring_hom : The injection inj_K_f is a ring homomorphism from K to A_K_f K. Hence we can regard K as a subring of A_K_f K.
number_field.inj_K.injective : The map inj_K is injective.
number_field.inj_K.ring_hom : The injection inj_K is a ring homomorphism from K to A_K K. Hence we can regard K as a subring of A_K K.

References #

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

Tags #

adèle ring, number field

The adèle ring of a number field #

We define the (finite) adèle ring of a number field K, with its topological ring structure.

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

Type

The finite adèle ring of K.

Equations

number_field.A_K_f K = finite_adele_ring' ↥(𝓞 K) K

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

Type

The adèle ring of K.

Equations

number_field.A_K K = (number_field.A_K_f K × ℝ ⊗ K)

@[protected, instance]

def number_field.pi.ring (n : ℕ) :

ring (fin n → ℝ)

Equations

number_field.pi.ring n = pi.ring

@[protected, instance]

noncomputable def number_field.pi.topological_space (n : ℕ) :

topological_space (fin n → ℝ)

Equations

number_field.pi.topological_space n = Pi.topological_space

@[protected, instance]

def number_field.pi.has_continuous_add (n : ℕ) :

has_continuous_add (fin n → ℝ)

@[protected, instance]

def number_field.pi.has_continuous_mul (n : ℕ) :

has_continuous_mul (fin n → ℝ)

@[protected, instance]

def number_field.pi.topological_semiring (n : ℕ) :

topological_semiring (fin n → ℝ)

@[protected, instance]

def number_field.pi.topological_ring (n : ℕ) :

topological_ring (fin n → ℝ)

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

(fin (finite_dimensional.finrank ℚ K) → ℚ) ≃ₗ[ℚ ] K

K is isomorphic to ℚ^(dim_ℚ(K)).

Equations

number_field.linear_equiv.Q_basis K = (finite_dimensional.fin_basis ℚ K).equiv_fun.symm

noncomputable def number_field.linear_map.Rn_to_R_tensor_Qn (n : ℕ) :

(fin n → ℝ) →ₗ[ℝ ] ℝ ⊗ (fin n → ℚ)

The natural linear map from ℝ^n to ℝ ⊗[ℚ] ℚ^n.

Equations

number_field.linear_map.Rn_to_R_tensor_Qn n = {to_fun := λ (x : fin n → ℝ), ∑ (m : fin n), ⇑(⇑(tensor_product.mk ℚ ℝ (fin n → ℚ)) (x m)) (λ (k : fin n), 1), map_add' := _, map_smul' := _}

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

ℝ ⊗ (fin (finite_dimensional.finrank ℚ K) → ℚ) →ₗ[ℝ ] ℝ ⊗ K

The map ℝ ⊗[ℚ] ℚ^(dim_ℚ(K)) → ℝ ⊗[ℚ] K obtained as a base change of linear_equiv.Q_basis.

Equations

number_field.linear_map.base_change K = linear_map.base_change ℝ (number_field.linear_equiv.Q_basis K).to_linear_map

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

(fin (finite_dimensional.finrank ℚ K) → ℝ) →ₗ[ℝ ] ℝ ⊗ K

The resulting linear map from ℝ^(dim_ℚ(K)) to ℝ ⊗[ℚ] K.

Equations

number_field.linear_map.Rn_to_R_tensor_K K = (number_field.linear_map.base_change K).comp (number_field.linear_map.Rn_to_R_tensor_Qn (finite_dimensional.finrank ℚ K))

@[protected, instance]

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

comm_ring (number_field.A_K_f K)

Equations

number_field.A_K_f.comm_ring K = finite_adele_ring'.comm_ring ↥(𝓞 K) K

@[protected, instance]

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

comm_ring (number_field.A_K K)

Equations

number_field.A_K.comm_ring K = prod.comm_ring

@[protected, instance]

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

inhabited (number_field.A_K_f K)

Equations

number_field.A_K_f.inhabited K = {default := 0}

@[protected, instance]

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

inhabited (number_field.A_K K)

Equations

number_field.A_K.inhabited K = {default := 0}

@[protected, instance]

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

topological_space (number_field.A_K_f K)

Equations

number_field.A_K_f.topological_space K = finite_adele_ring'.topological_space ↥(𝓞 K) K

@[protected, instance]

def number_field.A_K_f.topological_ring (K : Type) [field K] [number_field K] :

topological_ring (number_field.A_K_f K)

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

ring_topology (ℝ ⊗ K)

The topological ring structure on ℝ ⊗[ℚ] K.

Equations

number_field.infinite_adeles.ring_topology K = ring_topology.coinduced ⇑(number_field.linear_map.Rn_to_R_tensor_K K)

@[protected, instance]

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

topological_space (ℝ ⊗ K)

Equations

number_field.tensor_product.topological_space K = (number_field.infinite_adeles.ring_topology K).to_topological_space

@[protected, instance]

def number_field.tensor_product.topological_ring (K : Type) [field K] [number_field K] :

topological_ring (ℝ ⊗ K)

@[protected, instance]

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

topological_space (number_field.A_K K)

Equations

number_field.A_K.topological_space K = prod.topological_space

@[protected, instance]

def number_field.A_K.topological_ring (K : Type) [field K] [number_field K] :

topological_ring (number_field.A_K K)

theorem number_field.int.not_field :

The ring ℤ is not a field.

theorem number_field.ring_of_integers.not_field (K : Type) [field K] [number_field K] :

¬is_field ↥(𝓞 K)

The ring of integers of a number field is not a field.

@[protected, instance]

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

inhabited (maximal_spectrum ↥(𝓞 K))

There exists a nonzero prime ideal of the ring of integers of a number field.

Equations

number_field.maximal_spectrum.inhabited K = let M : ideal ↥(𝓞 K) := classical.some _, hM : (classical.some _).is_maximal := _ in {default := {as_ideal := M, is_prime := _, ne_bot := _}}

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

K → number_field.A_K_f K

The map from K to A_K_f K sending k ∈ K ↦ (k)_v.

Equations

number_field.inj_K_f K = inj_K ↥(𝓞 K) K

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

function.injective (number_field.inj_K_f K)

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

K →+* number_field.A_K_f K

The injection inj_K_f is a ring homomorphism from K to A_K_f K. Hence we can regard K as a subring of A_K_f K.

Equations

number_field.inj_K_f.ring_hom K = inj_K.ring_hom ↥(𝓞 K) K

theorem number_field.inj_K_f.ring_hom.v_comp (K : Type) [field K] [number_field K] (v : maximal_spectrum ↥(𝓞 K)) (k : K) :

(⇑(number_field.inj_K_f.ring_hom K) k).val v = ↑k

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

K → number_field.A_K K

The map from K to A_K K sending k ∈ K ↦ ((k)_v, 1 ⊗ k).

Equations

number_field.inj_K K = λ (x : K), (number_field.inj_K_f K x, ⇑algebra.tensor_product.include_right x)

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

function.injective (number_field.inj_K K)

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

K →+* number_field.A_K K

The injection inj_K is a ring homomorphism from K to A_K K. Hence we can regard K as a subring of A_K K.

Equations

number_field.inj_K.ring_hom K = (number_field.inj_K_f.ring_hom K).prod ↑algebra.tensor_product.include_right