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.instFintypeClassGroupSubtypeMemSubalgebraPolynomialToSemiringToDivisionSemiringToSemifieldToCommSemiringCommRingToCommRingToSemiringInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingToCommRingToEuclideanDomainInstIsDomainSubtypeMemSubalgebraPolynomialToSemiringToDivisionSemiringToSemifieldToCommSemiringCommRingToCommRingToSemiringInstMembershipInstSetLikeSubalgebraRingOfIntegersToSemiring (Fq : Type) (F : Type) [Field Fq] [Fintype Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] [IsSeparable (RatFunc Fq) F] : Fintype (ClassGroup { x // x ∈ FunctionField.ringOfIntegers Fq F })

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

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

theorem FunctionField.classNumber_eq_one_iff (Fq : Type) (F : Type) [Field Fq] [Fintype Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] [IsSeparable (RatFunc Fq) F] : FunctionField.classNumber Fq F = 1 ↔ IsPrincipalIdealRing { x // x ∈ FunctionField.ringOfIntegers Fq F }

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