Function fields

This file defines a function field and the ring of integers corresponding to it.

Main definitions

• FunctionField Fq F states that F is a function field over the (finite) field Fq, i.e. it is a finite extension of the field of rational functions in one variable over Fq.
• FunctionField.ringOfIntegers defines the ring of integers corresponding to a function field as the integral closure of Fq[X] in the function field.
• FunctionField.inftyValuation : The place at infinity on Fq(t) is the nonarchimedean valuation on Fq(t) with uniformizer 1/t.
• FunctionField.FqtInfty : The completion Fq((t⁻¹)) of Fq(t) with respect to the valuation at infinity.

Implementation notes

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice. We also omit assumptions like Finite Fq or IsScalarTower Fq[X] (FractionRing Fq[X]) F in definitions, adding them back in lemmas when they are needed.

References

• [D. Marcus, Number Fields][marcus1977number]
• [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
• [P. Samuel, Algebraic Theory of Numbers][samuel1970algebraic]

Tags

function field, ring of integers

@[inline, reducible]

abbrev FunctionField (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (RatFunc Fq) F] : Prop

F is a function field over the finite field Fq if it is a finite extension of the field of rational functions in one variable over Fq.

Note that F can be a function field over multiple, non-isomorphic, Fq.

Equations

• FunctionField Fq F = FiniteDimensional (RatFunc Fq) F

theorem functionField_iff (Fq : Type) (F : Type) [Field Fq] [Field F] (Fqt : Type u_1) [Field Fqt] [Algebra (Polynomial Fq) Fqt] [IsFractionRing (Polynomial Fq) Fqt] [Algebra (RatFunc Fq) F] [Algebra Fqt F] [Algebra (Polynomial Fq) F] [IsScalarTower (Polynomial Fq) Fqt F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] : FunctionField Fq F ↔ FiniteDimensional Fqt F

F is a function field over Fq iff it is a finite extension of Fq(t).

theorem algebraMap_injective (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] : Function.Injective ⇑(algebraMap (Polynomial Fq) F)

def FunctionField.ringOfIntegers (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] : Subalgebra (Polynomial Fq) F

The function field analogue of NumberField.ringOfIntegers: FunctionField.ringOfIntegers Fq Fqt F is the integral closure of Fq[t] in F.

We don't actually assume F is a function field over Fq in the definition, only when proving its properties.

Equations

• FunctionField.ringOfIntegers Fq F = integralClosure (Polynomial Fq) F

instance FunctionField.ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomialToSemiringToDivisionSemiringToSemifieldToCommSemiringCommRingToCommRingToSemiringInstMembershipInstSetLikeSubalgebraRingOfIntegersToSemiring (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] : IsDomain ↥(FunctionField.ringOfIntegers Fq F)

Equations

• (_ : IsDomain ↥(FunctionField.ringOfIntegers Fq F)) = (_ : IsDomain ↥(FunctionField.ringOfIntegers Fq F))

instance FunctionField.ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomialToSemiringToDivisionSemiringToSemifieldToCommSemiringCommRingToCommRingToSemiringInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommSemiringToCommSemiringToAlgebraId (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] : IsIntegralClosure (↥(FunctionField.ringOfIntegers Fq F)) (Polynomial Fq) F

Equations

• (_ : IsIntegralClosure (↥(FunctionField.ringOfIntegers Fq F)) (Polynomial Fq) F) = (_ : IsIntegralClosure (↥(integralClosure (Polynomial Fq) F)) (Polynomial Fq) F)

theorem FunctionField.ringOfIntegers.algebraMap_injective (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] : Function.Injective ⇑(algebraMap (Polynomial Fq) ↥(FunctionField.ringOfIntegers Fq F))

theorem FunctionField.ringOfIntegers.not_isField (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] : ¬IsField ↥(FunctionField.ringOfIntegers Fq F)

instance FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomialToSemiringToDivisionSemiringToSemifieldToCommSemiringCommRingToCommRingToSemiringInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingToAlgebraToCommSemiringId (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] : IsFractionRing (↥(FunctionField.ringOfIntegers Fq F)) F

Equations

• (_ : IsFractionRing (↥(FunctionField.ringOfIntegers Fq F)) F) = (_ : IsFractionRing (↥(integralClosure (Polynomial Fq) F)) F)

instance FunctionField.ringOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraPolynomialToSemiringToDivisionSemiringToSemifieldToCommSemiringCommRingToCommRingToSemiringInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRing (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] : IsIntegrallyClosed ↥(FunctionField.ringOfIntegers Fq F)

Equations

• (_ : IsIntegrallyClosed ↥(FunctionField.ringOfIntegers Fq F)) = (_ : IsIntegrallyClosed ↥(integralClosure (Polynomial Fq) F))

instance FunctionField.ringOfIntegers.instIsNoetherianPolynomialToSemiringToDivisionSemiringToSemifieldSubtypeMemSubalgebraToCommSemiringCommRingToCommRingToSemiringInstMembershipInstSetLikeSubalgebraRingOfIntegersSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToCommRingInstModuleSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToNonAssocSemiringToSubsemiring (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] [IsSeparable (RatFunc Fq) F] : IsNoetherian (Polynomial Fq) ↥(FunctionField.ringOfIntegers Fq F)

Equations

• (_ : IsNoetherian (Polynomial Fq) ↥(FunctionField.ringOfIntegers Fq F)) = (_ : IsNoetherian (Polynomial Fq) ↥(FunctionField.ringOfIntegers Fq F))

instance FunctionField.ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialToSemiringToDivisionSemiringToSemifieldToCommSemiringCommRingToCommRingToSemiringInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRing (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] [IsSeparable (RatFunc Fq) F] : IsDedekindDomain ↥(FunctionField.ringOfIntegers Fq F)

Equations

• (_ : IsDedekindDomain ↥(FunctionField.ringOfIntegers Fq F)) = (_ : IsDedekindDomain ↥(FunctionField.ringOfIntegers Fq F))

The place at infinity on Fq(t)

def FunctionField.inftyValuationDef (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] (r : RatFunc Fq) : WithZero (Multiplicative ℤ)

The valuation at infinity is the nonarchimedean valuation on Fq(t) with uniformizer 1/t. Explicitly, if f/g ∈ Fq(t) is a nonzero quotient of polynomials, its valuation at infinity is Multiplicative.ofAdd(degree(f) - degree(g)).

Equations

• FunctionField.inftyValuationDef Fq r = if r = 0 then 0 else ↑(Multiplicative.ofAdd (RatFunc.intDegree r))

theorem FunctionField.InftyValuation.map_zero' (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : FunctionField.inftyValuationDef Fq 0 = 0

theorem FunctionField.InftyValuation.map_one' (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : FunctionField.inftyValuationDef Fq 1 = 1

theorem FunctionField.InftyValuation.map_mul' (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] (x : RatFunc Fq) (y : RatFunc Fq) : FunctionField.inftyValuationDef Fq (x * y) = FunctionField.inftyValuationDef Fq x * FunctionField.inftyValuationDef Fq y

theorem FunctionField.InftyValuation.map_add_le_max' (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] (x : RatFunc Fq) (y : RatFunc Fq) : FunctionField.inftyValuationDef Fq (x + y) ≤ max (FunctionField.inftyValuationDef Fq x) (FunctionField.inftyValuationDef Fq y)

@[simp]

theorem FunctionField.inftyValuation_of_nonzero (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {x : RatFunc Fq} (hx : x ≠ 0) : FunctionField.inftyValuationDef Fq x = ↑(Multiplicative.ofAdd (RatFunc.intDegree x))

def FunctionField.inftyValuation (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : Valuation (RatFunc Fq) (WithZero (Multiplicative ℤ))

The valuation at infinity on Fq(t).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FunctionField.inftyValuation_apply (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {x : RatFunc Fq} : (FunctionField.inftyValuation Fq) x = FunctionField.inftyValuationDef Fq x

@[simp]

theorem FunctionField.inftyValuation.C (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {k : Fq} (hk : k ≠ 0) : FunctionField.inftyValuationDef Fq (RatFunc.C k) = ↑(Multiplicative.ofAdd 0)

@[simp]

theorem FunctionField.inftyValuation.X (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : FunctionField.inftyValuationDef Fq RatFunc.X = ↑(Multiplicative.ofAdd 1)

@[simp]

theorem FunctionField.inftyValuation.polynomial (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {p : Polynomial Fq} (hp : p ≠ 0) : FunctionField.inftyValuationDef Fq ((algebraMap (Polynomial Fq) (RatFunc Fq)) p) = ↑(Multiplicative.ofAdd ↑(Polynomial.natDegree p))

def FunctionField.inftyValuedFqt (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : Valued (RatFunc Fq) (WithZero (Multiplicative ℤ))

The valued field Fq(t) with the valuation at infinity.

Equations

• FunctionField.inftyValuedFqt Fq = Valued.mk' (FunctionField.inftyValuation Fq)

theorem FunctionField.inftyValuedFqt.def (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {x : RatFunc Fq} : Valued.v x = FunctionField.inftyValuationDef Fq x

def FunctionField.FqtInfty (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : Type

The completion Fq((t⁻¹)) of Fq(t) with respect to the valuation at infinity.

Equations

• FunctionField.FqtInfty Fq = UniformSpace.Completion (RatFunc Fq)

instance FunctionField.instFieldFqtInftyRatFuncToCommRing (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : Field (FunctionField.FqtInfty Fq)

Equations

• FunctionField.instFieldFqtInftyRatFuncToCommRing Fq = UniformSpace.Completion.instField

instance FunctionField.instInhabitedFqtInftyRatFuncToCommRing (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : Inhabited (FunctionField.FqtInfty Fq)

Equations

• FunctionField.instInhabitedFqtInftyRatFuncToCommRing Fq = { default := 0 }

instance FunctionField.valuedFqtInfty (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] : Valued (FunctionField.FqtInfty Fq) (WithZero (Multiplicative ℤ))

The valuation at infinity on k(t) extends to a valuation on FqtInfty.

Equations

• FunctionField.valuedFqtInfty Fq = Valued.valuedCompletion

theorem FunctionField.valuedFqtInfty.def (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {x : FunctionField.FqtInfty Fq} : Valued.v x = Valued.extension x