# 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] [] [Algebra (RatFunc Fq) F] :

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
Instances For
theorem functionField_iff (Fq : Type) (F : Type) [Field Fq] [] (Fqt : Type u_1) [Field Fqt] [Algebra () Fqt] [IsFractionRing () Fqt] [Algebra (RatFunc Fq) F] [Algebra Fqt F] [Algebra () F] [IsScalarTower () Fqt F] [IsScalarTower () (RatFunc Fq) 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] [] [Algebra () F] [Algebra (RatFunc Fq) F] [IsScalarTower () (RatFunc Fq) F] :
def FunctionField.ringOfIntegers (Fq : Type) (F : Type) [Field Fq] [] [Algebra () 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
Instances For
Equations
• =
Equations
• =
Equations
• =
Equations
• =

### The place at infinity on Fq(t) #

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
• = if r = 0 then 0 else (Multiplicative.ofAdd )
Instances For
@[simp]
theorem FunctionField.inftyValuation_of_nonzero (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {x : RatFunc Fq} (hx : x 0) :

The valuation at infinity on Fq(t).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[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 : } (hp : p 0) :
FunctionField.inftyValuationDef Fq ((algebraMap () (RatFunc Fq)) p) = (Multiplicative.ofAdd )

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

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

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

Equations
Instances For
Equations
• = UniformSpace.Completion.instField
Equations
• = { default := 0 }

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

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