mathlib documentation

ideles / examples

Examples #

We instantiate some concrete examples of the definitions formalized in this project:

We compute the 2-adic valuation of some elements of ℤ and ℚ.
We define the finite adèle ring and finite idèle group of the Dedekind domains ℤ and ℤ[i].
We define the (finite) adèle ring and (finite) idèle group of the number field ℚ.

def v2 :

maximal_spectrum ℤ

The ideal generated by 2, as a maximal ideal of ℤ.

Equations

v2 = {as_ideal := ideal.span {2}, is_prime := v2._proof_5, ne_bot := v2._proof_6}

noncomputable def v2_int_adic_valuation :

valuation ℤ (with_zero (multiplicative ℤ))

The 2-adic valuation on ℤ.

Equations

v2_int_adic_valuation = v2.int_valuation

noncomputable def v2_adic_valuation :

valuation ℚ (with_zero (multiplicative ℤ))

The 2-adic valuation on ℚ.

Equations

v2_adic_valuation = v2.valuation

def finite_adeles_Z :

Type

The finite adèle ring of ℤ.

Equations

finite_adeles_Z = finite_adele_ring' ℤ ℚ

@[protected, instance]

noncomputable def finite_adeles_Z.inhabited :

inhabited finite_adeles_Z

Equations

finite_adeles_Z.inhabited = {default := inj_K ℤ ℚ 0}

def finite_ideles_Z :

Type

The finite idèle group of ℤ.

Equations

finite_ideles_Z = finite_idele_group' ℤ ℚ

@[protected, instance]

noncomputable def finite_ideles_Z.inhabited :

inhabited finite_ideles_Z

Equations

finite_ideles_Z.inhabited = {default := inj_units_K ℤ ℚ 1}

def finite_adeles_Q :

Type

The finite adèle ring of ℚ.

Equations

finite_adeles_Q = number_field.A_K_f ℚ

@[protected, instance]

noncomputable def finite_adeles_Q.inhabited :

inhabited finite_adeles_Q

Equations

finite_adeles_Q.inhabited = {default := number_field.inj_K_f ℚ 0}

def adeles_Q :

Type

The adèle ring of ℚ.

Equations

adeles_Q = number_field.A_K ℚ

@[protected, instance]

noncomputable def adeles_Q.inhabited :

inhabited adeles_Q

Equations

adeles_Q.inhabited = {default := number_field.inj_K ℚ 0}

def finite_ideles_Q :

Type

The finite idèle group of ℚ.

Equations

finite_ideles_Q = number_field.I_K_f ℚ

@[protected, instance]

noncomputable def finite_ideles_Q.inhabited :

inhabited finite_ideles_Q

Equations

finite_ideles_Q.inhabited = {default := number_field.inj_units_K_f ℚ 1}

def ideles_Q :

Type

The idèle group of ℚ.

Equations

ideles_Q = number_field.I_K ℚ

@[protected, instance]

noncomputable def ideles_Q.inhabited :

inhabited ideles_Q

Equations

ideles_Q.inhabited = {default := number_field.inj_units_K ℚ 1}

def finite_adeles_Zi :

Type

The finite adèle ring of ℤ[i].

Equations

finite_adeles_Zi = finite_adele_ring' gaussian_int (fraction_ring gaussian_int)

@[protected, instance]

noncomputable def finite_adeles_Zi.inhabited :

inhabited finite_adeles_Zi

Equations

finite_adeles_Zi.inhabited = {default := inj_K gaussian_int (fraction_ring gaussian_int) 0}

def finite_ideles_Zi :

Type

The finite idèle group of ℤ[i].

Equations

finite_ideles_Zi = finite_idele_group' gaussian_int (fraction_ring gaussian_int)

@[protected, instance]

noncomputable def finite_ideles_Zi.inhabited :

inhabited finite_ideles_Zi

Equations

finite_ideles_Zi.inhabited = {default := inj_units_K gaussian_int (fraction_ring gaussian_int) 1}