The ring of adèles of a function field #

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

Main definitions #

function_field.A_F_f : The finite adèle ring of the function field F.
function_field.A_F : The adèle ring of the function field F.
function_field.inj_F_f : The map from K to A_F_f k F sending k ∈ K ↦ (k)_v
function_field.inj_F : The map from K to A_F k F sending k ∈ K ↦ ((k)_v, 1 ⊗ k).

Main results #

function_field.inj_F_f.injective : The map inj_F_f is injective.
function_field.inj_F_f.ring_hom : The injection inj_F_f is a ring homomorphism from K to A_F_f k F. Hence we can regard K as a subring of A_F_f k F.
function_field.inj_F.injective : The map inj_F is injective.
function_field.inj_F.ring_hom : The injection inj_F is a ring homomorphism from K to A_F k F. Hence we can regard K as a subring of A_F k F.

References #

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

Tags #

adèle ring, function field

The adèle ring of a function field #

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

source

@[protected, instance]

noncomputable def function_field.kt_infty.algebra (k : Type) [field k] :

algebra (ratfunc k) (kt_infty k)

Equations

function_field.kt_infty.algebra k = uniform_space.completion.coe_ring_hom.to_algebra

source

def function_field.A_F_f (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

Type

The finite adèle ring of F.

Equations

function_field.A_F_f k F = finite_adele_ring' ↥(function_field.ring_of_integers k F) F

source

def function_field.A_F (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

Type

The finite adèle ring of F.

Equations

function_field.A_F k F = (function_field.A_F_f k F × kt_infty k ⊗ F)

source

noncomputable def function_field.linear_equiv.kt_basis (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

(fin (finite_dimensional.finrank (ratfunc k) F) → ratfunc k) ≃ₗ[ratfunc k] F

F is isomorphic to k(t)^(dim_(F_q(t))(F)).

Equations

function_field.linear_equiv.kt_basis k F = (finite_dimensional.fin_basis (ratfunc k) F).equiv_fun.symm

source

noncomputable def function_field.linear_map.kt_inftyn_to_kt_infty_tensor_ktn (k : Type) [field k] (n : ℕ) :

(fin n → kt_infty k) →ₗ[kt_infty k] kt_infty k ⊗ (fin n → ratfunc k)

The natural linear map from k((t⁻¹))^n to k((t⁻¹)) ⊗[k(t)] k(t)^n.

Equations

function_field.linear_map.kt_inftyn_to_kt_infty_tensor_ktn k n = {to_fun := λ (x : fin n → kt_infty k), ∑ (m : fin n), ⇑(⇑(tensor_product.mk (ratfunc k) (kt_infty k) (fin n → ratfunc k)) (x m)) (λ (m : fin n), 1), map_add' := _, map_smul' := _}

source

noncomputable def function_field.linear_map.base_change (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

kt_infty k ⊗ (fin (finite_dimensional.finrank (ratfunc k) F) → ratfunc k) →ₗ[kt_infty k] kt_infty k ⊗ F

The linear map from k((t⁻¹)) ⊗[k(t)] k(t)^(dim_(F_q(t))(F)) to k((t⁻¹)) ⊗[k(t)] F obtained as a base change of linear_equiv.kt_basis.

Equations

function_field.linear_map.base_change k F = linear_map.base_change (kt_infty k) (function_field.linear_equiv.kt_basis k F).to_linear_map

source

noncomputable def function_field.linear_map.kt_inftyn_to_kt_infty_tensor_F (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

(fin (finite_dimensional.finrank (ratfunc k) F) → kt_infty k) →ₗ[kt_infty k] kt_infty k ⊗ F

The resulting linear map from k((t⁻¹))^(dim_(F_q(t))(F)) to k((t⁻¹)) ⊗[k(t)] F.

Equations

function_field.linear_map.kt_inftyn_to_kt_infty_tensor_F k F = (function_field.linear_map.base_change k F).comp (function_field.linear_map.kt_inftyn_to_kt_infty_tensor_ktn k (finite_dimensional.finrank (ratfunc k) F))

source

@[protected, instance]

noncomputable def function_field.A_F_f.comm_ring (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

comm_ring (function_field.A_F_f k F)

Equations

function_field.A_F_f.comm_ring k F = finite_adele_ring'.comm_ring ↥(function_field.ring_of_integers k F) F

source

@[protected, instance]

noncomputable def function_field.A_F.comm_ring (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

comm_ring (function_field.A_F k F)

Equations

function_field.A_F.comm_ring k F = prod.comm_ring

source

@[protected, instance]

noncomputable def function_field.A_F_f.inhabited (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

inhabited (function_field.A_F_f k F)

Equations

function_field.A_F_f.inhabited k F = {default := 0}

source

@[protected, instance]

noncomputable def function_field.A_F.inhabited (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

inhabited (function_field.A_F k F)

Equations

function_field.A_F.inhabited k F = {default := 0}

source

@[protected, instance]

noncomputable def function_field.A_F_f.topological_space (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

topological_space (function_field.A_F_f k F)

Equations

function_field.A_F_f.topological_space k F = finite_adele_ring'.topological_space ↥(function_field.ring_of_integers k F) F

source

@[protected, instance]

def function_field.A_F_f.topological_ring (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

topological_ring (function_field.A_F_f k F)

source

noncomputable def function_field.infinite_adeles.ring_topology (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

ring_topology (kt_infty k ⊗ F)

The topological ring structure on the infinite places of F.

Equations

function_field.infinite_adeles.ring_topology k F = ring_topology.coinduced ⇑(function_field.linear_map.kt_inftyn_to_kt_infty_tensor_F k F)

source

@[protected, instance]

noncomputable def function_field.tensor_product.topological_space (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

topological_space (kt_infty k ⊗ F)

Equations

function_field.tensor_product.topological_space k F = (function_field.infinite_adeles.ring_topology k F).to_topological_space

source

@[protected, instance]

def function_field.tensor_product.topological_ring (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

topological_ring (kt_infty k ⊗ F)

source

@[protected, instance]

noncomputable def function_field.A_F.topological_space (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

topological_space (function_field.A_F k F)

Equations

function_field.A_F.topological_space k F = prod.topological_space

source

@[protected, instance]

def function_field.A_F.topological_ring (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

topological_ring (function_field.A_F k F)

source

theorem function_field.algebra_map_injective (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

function.injective ⇑(algebra_map k[X] ↥(function_field.ring_of_integers k F))

source

theorem function_field.kX_not_is_field (k : Type) [field k] :

¬is_field k[X]

The ring of integers of polynomials over k is not a field.

source

theorem function_field.not_is_field (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

¬is_field ↥(function_field.ring_of_integers k F)

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

source

@[protected, instance]

noncomputable def function_field.maximal_spectrum.inhabited (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

inhabited (maximal_spectrum ↥(function_field.ring_of_integers k F))

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

Equations

function_field.maximal_spectrum.inhabited k F = let M : ideal ↥(function_field.ring_of_integers k F) := classical.some _, hM : (classical.some _).is_maximal := _ in {default := {as_ideal := M, is_prime := _, ne_bot := _}}

source

noncomputable def function_field.inj_F_f (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

F → function_field.A_F_f k F

The map from F to A_F_f k F sending x ∈ F ↦ (x)_v.

Equations

function_field.inj_F_f k F = inj_K ↥(function_field.ring_of_integers k F) F

source

theorem function_field.inj_F_f.injective (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

function.injective (function_field.inj_F_f k F)

source

noncomputable def function_field.inj_F_f.ring_hom (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

F →+* function_field.A_F_f k F

The injection inj_F_f is a ring homomorphism from F to A_F_f k F. Hence we can regard F as a subring of A_F_f k F.

Equations

function_field.inj_F_f.ring_hom k F = inj_K.ring_hom ↥(function_field.ring_of_integers k F) F

source

theorem function_field.inj_F_f.ring_hom.v_comp (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] (v : maximal_spectrum ↥(function_field.ring_of_integers k F)) (x : F) :

(⇑(function_field.inj_F_f.ring_hom k F) x).val v = ↑x

source

noncomputable def function_field.inj_F (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

F → function_field.A_F k F

The map from F to A_F k F sending x ∈ F ↦ ((x)_v, 1 ⊗ x).

Equations

function_field.inj_F k F = λ (x : F), (function_field.inj_F_f k F x, ⇑algebra.tensor_product.include_right x)

source

theorem function_field.inj_F.injective (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

function.injective (function_field.inj_F k F)

source

noncomputable def function_field.inj_F.ring_hom (k F : Type) [field k] [field F] [algebra k[X] F] [algebra (ratfunc k) F] [function_field k F] [is_scalar_tower k[X] (ratfunc k) F] [is_separable (ratfunc k) F] :

F →+* function_field.A_F k F

The injection inj_F is a ring homomorphism from F to A_F k F. Hence we can regard F as a subring of A_F k F.

Equations

function_field.inj_F.ring_hom k F = (function_field.inj_F_f.ring_hom k F).prod ↑algebra.tensor_product.include_right