Class numbers of function fields #

This file defines the class number of a function field as the (finite) cardinality of the class group of its ring of integers. It also proves some elementary results on the class number.

Main definitions #

function_field.class_number: the class number of a function field is the (finite) cardinality of the class group of its ring of integers

source

@[protected, instance]

noncomputable def function_field.ring_of_integers.class_group.fintype (Fq F : Type) [field Fq] [fintype Fq] [field F] [algebra Fq[X] F] [algebra (ratfunc Fq) F] [is_scalar_tower Fq[X] (ratfunc Fq) F] [function_field Fq F] [is_separable (ratfunc Fq) F] :

fintype (class_group ↥(function_field.ring_of_integers Fq F) F)

Equations

function_field.ring_of_integers.class_group.fintype Fq F = class_group.fintype_of_admissible_of_finite (ratfunc Fq) F polynomial.card_pow_degree_is_admissible

source

noncomputable def function_field.class_number (Fq F : Type) [field Fq] [fintype Fq] [field F] [algebra Fq[X] F] [algebra (ratfunc Fq) F] [is_scalar_tower Fq[X] (ratfunc Fq) F] [function_field Fq F] [is_separable (ratfunc Fq) F] :

ℕ

The class number in a function field is the (finite) cardinality of the class group.

Equations

function_field.class_number Fq F = fintype.card (class_group ↥(function_field.ring_of_integers Fq F) F)

source

theorem function_field.class_number_eq_one_iff (Fq F : Type) [field Fq] [fintype Fq] [field F] [algebra Fq[X] F] [algebra (ratfunc Fq) F] [is_scalar_tower Fq[X] (ratfunc Fq) F] [function_field Fq F] [is_separable (ratfunc Fq) F] :

function_field.class_number Fq F = 1 ↔ is_principal_ideal_ring ↥(function_field.ring_of_integers Fq F)

The class number of a function field is 1 iff the ring of integers is a PID.