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öhlich, Algebraic Number Theory][cassels1967algebraic]
• [P. Samuel, Algebraic Theory of Numbers][samuel1967]

Tags

function field, ring of integers

@[reducible, inline]

abbrev FunctionField (Fq : Type u_1) (F : Type u_2) [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 u_1) (F : Type u_2) [Field Fq] [Field F] (Fqt : Type u_3) [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 FunctionField.algebraMap_injective (Fq : Type u_1) (F : Type u_2) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] : Function.Injective ⇑(algebraMap (Polynomial Fq) F)

@[deprecated FunctionField.algebraMap_injective (since := "2025-03-03")]

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

Alias of FunctionField.algebraMap_injective.

def FunctionField.ringOfIntegers (Fq : Type u_1) (F : Type u_2) [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.instIsDomainSubtypeMemSubalgebraPolynomial (Fq : Type u_1) (F : Type u_2) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] : IsDomain ↥(ringOfIntegers Fq F)

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

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

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

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

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

instance FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc (Fq : Type u_1) (F : Type u_2) [Field 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] : IsNoetherian (Polynomial Fq) ↥(ringOfIntegers Fq F)

instance FunctionField.ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc (Fq : Type u_1) (F : Type u_2) [Field 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] : IsDedekindDomain ↥(ringOfIntegers Fq F)

The place at infinity on Fq(t)

def FunctionField.inftyValuationDef (Fq : Type u_1) [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 r.intDegree)

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

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

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

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

@[simp]

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

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

The valuation at infinity on Fq(t).

Equations

• FunctionField.inftyValuation Fq = { toFun := FunctionField.inftyValuationDef Fq, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

@[simp]

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

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

@[simp]

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

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

def FunctionField.inftyValuedFqt (Fq : Type u_1) [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 u_1) [Field Fq] [DecidableEq (RatFunc Fq)] {x : RatFunc Fq} : Valued.v x = inftyValuationDef Fq x

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

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

Equations

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

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

Equations

• FunctionField.instFieldFqtInfty Fq = UniformSpace.Completion.instField

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

Equations

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

instance FunctionField.valuedFqtInfty (Fq : Type u_1) [Field Fq] [DecidableEq (RatFunc Fq)] : Valued (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 u_1) [Field Fq] [DecidableEq (RatFunc Fq)] {x : FqtInfty Fq} : Valued.v x = Valued.extension x