Class numbers of function fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (polynomial Fq) F] [algebra (ratfunc Fq) F] [is_scalar_tower (polynomial Fq) (ratfunc Fq) F] [function_field Fq F] [is_separable (ratfunc Fq) F] :

fintype (class_group ↥(function_field.ring_of_integers Fq 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 (polynomial Fq) F] [algebra (ratfunc Fq) F] [is_scalar_tower (polynomial Fq) (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))

source

theorem function_field.class_number_eq_one_iff (Fq F : Type) [field Fq] [fintype Fq] [field F] [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F] [is_scalar_tower (polynomial Fq) (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.