The group of idèles of a function field #
We define the group of finite idèles and the group of idèles of a function field F, both of which
are topological commutative groups.
We also prove that F* can be regarded as a subgroup of I_F_f and I_F and define the idèle
class group of F as the quotient I_F/F*. We then show that the ideal class group of F is
isomorphic to an explicit quotient of C_F as topological groups, by constructing a continuous
surjective group homomorphism from C_F to the ideal class group Cl(F) of F and
computing its kernel.
Main definitions #
function_field.I_F_f: The finite idèle group of the function fieldF.function_field.I_F: The idèle group of the function fieldF.function_field.C_F: The idèle class group of the function fieldF.function_field.C_F.map_to_class_group: The natural group homomorphism fromC_FtoCl(F).
Main results #
function_field.C_F.map_to_class_group.surjective: The natural mapC_F → Cl(F)is surjective.function_field.C_F.map_to_class_group.continuous: The natural mapC_F → Cl(F)is continuous.function_field.C_F.map_to_class_group.mem_kernel_iff: We compute the kernel ofC_F → Cl(F).
References #
Tags #
idèle group, number field, function field
The idèle group of a function field #
We define the (finite) idèle group of a function field F, with its topological group structure.
def
function_field.I_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 idèle group of the function field F.
Equations
- function_field.I_F_f k F = (function_field.A_F_f k F)ˣ
def
function_field.I_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 idèle group of the function field F.
Equations
- function_field.I_F k F = (function_field.A_F k F)ˣ
@[protected, instance]
noncomputable
def
function_field.I_F_f.comm_group
(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] :
Equations
@[protected, instance]
noncomputable
def
function_field.I_F.comm_group
(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_group (function_field.I_F k F)
Equations
@[protected, instance]
noncomputable
def
function_field.I_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] :
Equations
- function_field.I_F_f.inhabited k F = {default := 1}
@[protected, instance]
noncomputable
def
function_field.I_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.I_F k F)
Equations
- function_field.I_F.inhabited k F = {default := 1}
@[protected, instance]
noncomputable
def
function_field.I_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] :
@[protected, instance]
def
function_field.I_F_f.topological_group
(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] :
@[protected, instance]
noncomputable
def
function_field.I_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] :
Equations
@[protected, instance]
def
function_field.I_F.topological_group
(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] :
noncomputable
def
function_field.I_F.as_prod
(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_field.I_F k F ≃* function_field.I_F_f k F × (kt_infty k ⊗ F)ˣ
I_F is isomorphic to the product I_F_f × ((kt_infty k) ⊗[ratfunc k] F)*, as groups.
Equations
noncomputable
def
function_field.I_F.as_prod.homeo
(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_field.I_F k F ≃ₜ function_field.I_F_f k F × (kt_infty k ⊗ F)ˣ
I_F is homeomorphic to the product I_F_f × ((kt_infty k) ⊗[ratfunc k] F)*.
Equations
theorem
function_field.I_F.as_prod.continuous
{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] :
theorem
function_field.I_F.as_prod.continuous_inv
{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] :
noncomputable
def
function_field.I_F.mk
{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]
(x : function_field.I_F_f k F)
(u : (kt_infty k ⊗ F)ˣ) :
Construct an idèle of F given a finite idèle and a unit of (kt_infty k) ⊗[ratfunc k] F.
Equations
- function_field.I_F.mk x u = (function_field.I_F.as_prod k F).inv_fun (x, u)
noncomputable
def
function_field.I_F.fst
(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_field.I_F k F →* function_field.I_F_f k F
The projection from I_F to I_F_f, as a group homomorphism.
Equations
- function_field.I_F.fst k F = {to_fun := λ (x : function_field.I_F k F), ((function_field.I_F.as_prod k F).to_fun x).fst, map_one' := _, map_mul' := _}
theorem
function_field.I_F.fst.surjective
{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] :
The projection map I_F.fst is surjective.
theorem
function_field.I_F.fst.continuous
{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] :
The projection map I_F.fst is continuous.
theorem
function_field.right_inv
{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]
(x : Fˣ) :
(⇑(function_field.inj_F.ring_hom k F) x.val) * ⇑(function_field.inj_F.ring_hom k F) x.inv = 1
theorem
function_field.left_inv
{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]
(x : Fˣ) :
(⇑(function_field.inj_F.ring_hom k F) x.inv) * ⇑(function_field.inj_F.ring_hom k F) x.val = 1
noncomputable
def
function_field.inj_units_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.I_F k F
The map from F^* to I_F sending x to ((x)_v, 1 ⊗ x).
Equations
@[simp]
theorem
function_field.inj_units_F.map_one
{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_field.inj_units_F k F 1 = 1
@[simp]
theorem
function_field.inj_units_F.map_mul
{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]
(x y : Fˣ) :
function_field.inj_units_F k F (x * y) = (function_field.inj_units_F k F x) * function_field.inj_units_F k F y
noncomputable
def
function_field.inj_units_F.group_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.I_F k F
inj_units_F is a group homomorphism.
Equations
- function_field.inj_units_F.group_hom k F = {to_fun := function_field.inj_units_F k F _inst_7, map_one' := _, map_mul' := _}
theorem
function_field.inj_units_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] :
inj_units_F is injective.
def
function_field.C_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 idèle class group of F is the quotient of I_F by the group F* of principal idèles.
Equations
- function_field.C_F k F = (function_field.I_F k F ⧸ (function_field.inj_units_F.group_hom k F).range)
@[protected, instance]
noncomputable
def
function_field.C_F.comm_group
(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_group (function_field.C_F k F)
@[protected, instance]
noncomputable
def
function_field.C_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.C_F k F)
Equations
- function_field.C_F.inhabited k F = {default := 1}
@[protected, instance]
noncomputable
def
function_field.C_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] :
Equations
@[protected, instance]
def
function_field.C_F.topological_group
(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] :
noncomputable
def
function_field.v_comp_val
(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]
(x : function_field.I_F k F)
(v : maximal_spectrum ↥(function_field.ring_of_integers k F)) :
The v-adic absolute value of the vth component of the idèle x.
noncomputable
def
function_field.v_comp_inv
(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]
(x : function_field.I_F k F)
(v : maximal_spectrum ↥(function_field.ring_of_integers k F)) :
The v-adic absolute value of the inverse of the vth component of the idèle x.
theorem
function_field.I_F_f.restricted_product
(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]
(x : function_field.I_F_f k F) :
({v : maximal_spectrum ↥(function_field.ring_of_integers k F) | x.val.val v ∉ maximal_spectrum.adic_completion_integers F v} ∪ {v : maximal_spectrum ↥(function_field.ring_of_integers k F) | x.inv.val v ∉ maximal_spectrum.adic_completion_integers F 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
function_field.prod_val_inv_eq_one
(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]
(x : function_field.I_F k F)
(v : maximal_spectrum ↥(function_field.ring_of_integers k F)) :
theorem
function_field.valuation.prod_val_inv_eq_one
(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]
(x : function_field.I_F k F)
(v : maximal_spectrum ↥(function_field.ring_of_integers k F)) :
(function_field.v_comp_val k F x v) * function_field.v_comp_inv k F x v = 1
theorem
function_field.v_comp.ne_zero
(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]
(x : function_field.I_F k F)
(v : maximal_spectrum ↥(function_field.ring_of_integers k F)) :
theorem
function_field.I_F.restricted_product
(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]
(x : function_field.I_F k F) :
({v : maximal_spectrum ↥(function_field.ring_of_integers k F) | x.val.fst.val v ∉ maximal_spectrum.adic_completion_integers F v} ∪ {v : maximal_spectrum ↥(function_field.ring_of_integers k F) | x.inv.fst.val v ∉ maximal_spectrum.adic_completion_integers F 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
function_field.I_F.finite_exponents
(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]
(x : function_field.I_F k F) :
{v : maximal_spectrum ↥(function_field.ring_of_integers k F) | function_field.v_comp_val k F 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
function_field.I_F_f.map_to_fractional_ideals
(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_field.I_F_f k F →* (fractional_ideal (↥(function_field.ring_of_integers k F))⁰ F)ˣ
The natural map from I_F_f to the group of invertible fractional ideals of F, sending a
finite idèle x to the product ∏_v v^(val_v(x_v)), where val_v denotes the additive
v-adic valuation.
theorem
function_field.I_F_f.map_to_fractional_ideals.surjective
{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] :
I_F_f.map_to_fractional_ideals is surjective.
theorem
function_field.I_F_f.map_to_fractional_ideals.mem_kernel_iff
{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]
(x : function_field.I_F_f k F) :
⇑(function_field.I_F_f.map_to_fractional_ideals k F) x = 1 ↔ ∀ (v : maximal_spectrum ↥(function_field.ring_of_integers k F)), finite_idele.to_add_valuations ↥(function_field.ring_of_integers k F) F x v = 0
A finite idèle x is in the kernel of I_F_f.map_to_fractional_ideals if and only if
|x_v|_v = 1 for all v.
theorem
function_field.I_F_f.map_to_fractional_ideals.continuous
{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] :
I_F_f.map_to_fractional_ideals is continuous.
noncomputable
def
function_field.I_F.map_to_fractional_ideals
(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_field.I_F k F →* (fractional_ideal (↥(function_field.ring_of_integers k F))⁰ F)ˣ
The natural map from I_F to the group of invertible fractional ideals of F.
Equations
theorem
function_field.I_F.map_to_fractional_ideals.surjective
{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] :
I_F.map_to_fractional_ideals is surjective.
theorem
function_field.I_F.map_to_fractional_ideals.mem_kernel_iff
{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]
(x : function_field.I_F k F) :
⇑(function_field.I_F.map_to_fractional_ideals k F) x = 1 ↔ ∀ (v : maximal_spectrum ↥(function_field.ring_of_integers k F)), finite_idele.to_add_valuations ↥(function_field.ring_of_integers k F) F (⇑(function_field.I_F.fst k F) x) v = 0
An idèle x is in the kernel of I_F_f.map_to_fractional_ideals if and only if |x_v|_v = 1
for all v.
theorem
function_field.I_F.map_to_fractional_ideals.continuous
{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] :
I_F.map_to_fractional_ideals is continuous.
noncomputable
def
function_field.I_F_f.map_to_class_group
(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_field.I_F_f k F → class_group ↥(function_field.ring_of_integers k F) F
The map from I_F_f to the ideal class group of F induced by
I_F_f.map_to_fractional_ideals.
Equations
- function_field.I_F_f.map_to_class_group k F = λ (x : function_field.I_F_f k F), quotient_group.mk (⇑(function_field.I_F_f.map_to_fractional_ideals k F) x)
@[protected, instance]
def
function_field.class_group.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] :
Equations
@[protected, instance]
def
function_field.class_group.topological_group
(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] :
theorem
function_field.I_F_f.map_to_class_group.surjective
{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] :
theorem
function_field.I_F_f.map_to_class_group.continuous
{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] :
noncomputable
def
function_field.I_F.map_to_class_group
(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_field.I_F k F → class_group ↥(function_field.ring_of_integers k F) F
The map from I_F to the ideal class group of K induced by
I_F.map_to_fractional_ideals.
Equations
- function_field.I_F.map_to_class_group k F = λ (x : function_field.I_F k F), ⇑(quotient_group.mk' (to_principal_ideal ↥(function_field.ring_of_integers k F) F).range) (⇑(function_field.I_F.map_to_fractional_ideals k F) x)
theorem
function_field.I_F.map_to_class_group.surjective
{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] :
theorem
function_field.I_F.map_to_class_group.continuous
{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] :
theorem
function_field.I_F.map_to_class_group.map_one
{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] :
theorem
function_field.I_F.map_to_class_group.map_mul
{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]
(x y : function_field.I_F k F) :
function_field.I_F.map_to_class_group k F (x * y) = (function_field.I_F.map_to_class_group k F x) * function_field.I_F.map_to_class_group k F y
noncomputable
def
function_field.I_F.monoid_hom_to_class_group
{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] :
The map from I_F to the ideal class group of F induced by
I_F.map_to_fractional_ideals is a group homomorphism.
Equations
- function_field.I_F.monoid_hom_to_class_group = {to_fun := function_field.I_F.map_to_class_group k F _inst_7, map_one' := _, map_mul' := _}
theorem
function_field.I_F_f.unit_image.mul_inv
{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]
(x : Fˣ) :
(⇑(function_field.inj_F_f.ring_hom k F) x.val) * ⇑(function_field.inj_F_f.ring_hom k F) x.inv = 1
theorem
function_field.I_F_f.unit_image.inv_mul
{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]
(x : Fˣ) :
(⇑(function_field.inj_F_f.ring_hom k F) x.inv) * ⇑(function_field.inj_F_f.ring_hom k F) x.val = 1
theorem
function_field.I_F_f.map_to_fractional_ideal.map_units
{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]
(x : Fˣ) :
fractional_ideal.span_singleton (↥(function_field.ring_of_integers k F))⁰ ↑x = ↑(⇑(function_field.I_F_f.map_to_fractional_ideals k F) {val := ⇑(function_field.inj_F_f.ring_hom k F) x.val, inv := ⇑(function_field.inj_F_f.ring_hom k F) x.inv, val_inv := _, inv_val := _})
I_F_f.map_to_fractional_ideals sends the principal finite idèle (x)_v corresponding to
x ∈ F* to the principal fractional ideal generated by x.
theorem
function_field.I_F.map_to_fractional_ideals.map_units_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]
(x : Fˣ) :
I_F.map_to_fractional_ideals sends the principal idèle (x)_v corresponding to x ∈ F* to
the principal fractional ideal generated by x.
theorem
function_field.I_F.map_to_class_group.map_units_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]
(x : Fˣ) :
The kernel of I_F.map_to_fractional_ideals contains the principal idèles (x)_v, for
x ∈ F*.
theorem
function_field.I_F.map_to_fractional_ideals.apply
{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]
(x : function_field.I_F k F) :
↑(⇑(function_field.I_F.map_to_fractional_ideals k F) x) = ∏ᶠ (v : maximal_spectrum ↥(function_field.ring_of_integers k F)), ↑(v.as_ideal) ^ finite_idele.to_add_valuations ↥(function_field.ring_of_integers k F) F (⇑(function_field.I_F.fst k F) x) v
theorem
function_field.I_F.map_to_class_group.valuation_mem_kernel
{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]
(x : function_field.I_F k F)
(u : Fˣ)
(v : maximal_spectrum ↥(function_field.ring_of_integers k F))
(hux : fractional_ideal.span_singleton (↥(function_field.ring_of_integers k F))⁰ ↑u = ↑(⇑(function_field.I_F.map_to_fractional_ideals k F) x)) :
If the image of x ∈ I_F under I_F.map_to_class_group is the principal fractional ideal
generated by u ∈ F*, then for every maximal ideal v of the ring of integers of F,
|x_v|_v = |u|_v.
theorem
function_field.I_F.map_to_class_group.mem_kernel_iff
{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]
(x : function_field.I_F k F) :
function_field.I_F.map_to_class_group k F x = 1 ↔ ∃ (u : F) (hu : u ≠ 0), ∀ (v : maximal_spectrum ↥(function_field.ring_of_integers k F)), finite_idele.to_add_valuations ↥(function_field.ring_of_integers k F) F (⇑(function_field.I_F.fst k F) x) v = -with_zero.to_integer _
An element x ∈ I_F is in the kernel of C_F → Cl(F) if and only if there exist u ∈ F* and
y ∈ I_F such that x = u*y and |y_v|_v = 1 for all v.
noncomputable
def
function_field.C_F.map_to_class_group
(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] :
The map C_F → Cl(F) induced by I_F.map_to_class_group.
theorem
function_field.C_F.map_to_class_group.surjective
(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] :
The natural map C_F → Cl(F) is surjective.
theorem
function_field.C_F.map_to_class_group.continuous
(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] :
The natural map C_F → Cl(F) is continuous.
theorem
function_field.C_F.map_to_class_group.mem_kernel_iff
(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]
(x : function_field.C_F k F) :
⇑(function_field.C_F.map_to_class_group k F) x = 1 ↔ ∃ (u : F) (hu : u ≠ 0), ∀ (v : maximal_spectrum ↥(function_field.ring_of_integers k F)), finite_idele.to_add_valuations ↥(function_field.ring_of_integers k F) F (⇑(function_field.I_F.fst k F) (classical.some _)) v = -with_zero.to_integer _
An element x ∈ C_F is in the kernel of C_F → Cl(F) if and only if x comes from an idèle
of the form u*y, with u ∈ F* and |y_v|_v = 1 for all v.