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.
Instances For
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.