Documentation

Mathlib.NumberTheory.ClassNumber.FunctionField

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 #

source
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 ↥(FunctionField.ringOfIntegers Fq F))
Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
Instances For
    source
    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 ↥(FunctionField.ringOfIntegers Fq F)

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