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.

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)

noncomputable 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.

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)

noncomputable 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 exp (degree(f) - degree(g)).

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 = WithZero.exp x.intDegree

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

The valuation at infinity on Fq(t).

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

@[simp]

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

@[simp]

theorem FunctionField.inftyValuation.X (Fq : Type u_1) [Field Fq] [DecidableEq (RatFunc Fq)] : (inftyValuation Fq) RatFunc.X = WithZero.exp 1

theorem FunctionField.inftyValuation.X_zpow (Fq : Type u_1) [Field Fq] [DecidableEq (RatFunc Fq)] (m : ℤ) : (inftyValuation Fq) (RatFunc.X ^ m) = WithZero.exp m

theorem FunctionField.inftyValuation.X_inv (Fq : Type u_1) [Field Fq] [DecidableEq (RatFunc Fq)] : (inftyValuation Fq) (1 / RatFunc.X) = WithZero.exp (-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) = WithZero.exp ↑p.natDegree

instance FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation (Fq : Type u_1) [Field Fq] [DecidableEq (RatFunc Fq)] : (inftyValuation Fq).IsNontrivial

instance FunctionField.instIsTrivialOnWithZeroMultiplicativeIntRatFuncInftyValuation (Fq : Type u_1) [Field Fq] [DecidableEq (RatFunc Fq)] : Valuation.IsTrivialOn Fq (inftyValuation Fq)

@[implicit_reducible]

noncomputable 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.

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

@[implicit_reducible]

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

The uniform space structure on RatFunc Fq coming from the valuation at infinity.

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.

@[implicit_reducible]

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

@[implicit_reducible]

noncomputable instance FunctionField.FqtInfty.instAlgebraRatFunc (Fq : Type u_1) [Field Fq] [DecidableEq (RatFunc Fq)] : Algebra (RatFunc Fq) (FqtInfty Fq)

@[implicit_reducible]

noncomputable instance FunctionField.FqtInfty.instCoeRatFunc (Fq : Type u_1) [Field Fq] [DecidableEq (RatFunc Fq)] : Coe (RatFunc Fq) (FqtInfty Fq)

@[implicit_reducible]

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

@[implicit_reducible]

noncomputable 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.

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