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

• FunctionField.classNumber: the class number of a function field is the (finite) cardinality of the class group of its ring of integers

noncomputable instance FunctionField.RingOfIntegers.instFintypeClassGroupSubtypeMemSubalgebraPolynomialRingOfIntegers (Fq : Type u_1) (F : Type u_2) [Field Fq] [Fintype Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] [Algebra.IsSeparable (RatFunc Fq) F] : Fintype (ClassGroup ↥(FunctionField.ringOfIntegers Fq F))

Equations

• FunctionField.RingOfIntegers.instFintypeClassGroupSubtypeMemSubalgebraPolynomialRingOfIntegers Fq F = ClassGroup.fintypeOfAdmissibleOfFinite (RatFunc Fq) F Polynomial.cardPowDegreeIsAdmissible

noncomputable def FunctionField.classNumber (Fq : Type u_1) (F : Type u_2) [Field Fq] [Fintype Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] [Algebra.IsSeparable (RatFunc Fq) F] : ℕ

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

Equations

• FunctionField.classNumber Fq F = Fintype.card (ClassGroup ↥(FunctionField.ringOfIntegers Fq F))

theorem FunctionField.classNumber_eq_one_iff (Fq : Type u_1) (F : Type u_2) [Field Fq] [Fintype Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] [Algebra.IsSeparable (RatFunc Fq) F] : FunctionField.classNumber Fq F = 1 ↔ IsPrincipalIdealRing ↥(FunctionField.ringOfIntegers Fq F)

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