# mathlib3documentation

number_theory.function_field

# Function fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• function_field 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.
• function_field.ring_of_integers defines the ring of integers corresponding to a function field as the integral closure of Fq[X] in the function field.
• function_field.infty_valuation : The place at infinity on Fq(t) is the nonarchimedean valuation on Fq(t) with uniformizer 1/t.
• function_field.Fqt_infty : 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 is_scalar_tower Fq[X] (fraction_ring Fq[X]) F in definitions, adding them back in lemmas when they are needed.

## Tags #

function field, ring of integers

@[reducible]
def function_field (Fq 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.

@[protected]
theorem function_field_iff (Fq F : Type) [field Fq] [field F] (Fqt : Type u_1) [field Fqt] [algebra (polynomial Fq) Fqt] [ Fqt] [algebra (ratfunc Fq) F] [algebra Fqt F] [algebra (polynomial Fq) F] [ Fqt F] [ (ratfunc Fq) F] :
F F

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

noncomputable def function_field.ring_of_integers (Fq F : Type) [field Fq] [field F] [algebra (polynomial Fq) F] :

The function field analogue of number_field.ring_of_integers: function_field.ring_of_integers 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 ↥function_field.ring_of_integers
@[protected, instance]
@[protected, instance]
theorem function_field.ring_of_integers.not_is_field (Fq F : Type) [field Fq] [field F] [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F] [ (ratfunc Fq) F] :
@[protected, instance]
def function_field.ring_of_integers.is_fraction_ring (Fq F : Type) [field Fq] [field F] [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F] [ (ratfunc Fq) F] [ F] :
@[protected, instance]
@[protected, instance]
def function_field.ring_of_integers.is_noetherian (Fq F : Type) [field Fq] [field F] [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F] [ (ratfunc Fq) F] [ F] [is_separable (ratfunc Fq) F] :
@[protected, instance]

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

noncomputable def function_field.infty_valuation_def (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] (r : ratfunc Fq) :

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

Equations
@[simp]
theorem function_field.infty_valuation_of_nonzero (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {x : ratfunc Fq} (hx : x 0) :
noncomputable def function_field.infty_valuation (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

The valuation at infinity on Fq(t).

Equations
@[simp]
@[simp]
theorem function_field.infty_valuation.C (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {k : Fq} (hk : k 0) :
@[simp]
@[simp]
theorem function_field.infty_valuation.polynomial (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {p : polynomial Fq} (hp : p 0) :
noncomputable def function_field.infty_valued_Fqt (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

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

Equations

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

Equations
Instances for function_field.Fqt_infty
@[protected, instance]
noncomputable def function_field.Fqt_infty.field (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :
Equations
@[protected, instance]
noncomputable def function_field.Fqt_infty.inhabited (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :
Equations
@[protected, instance]
noncomputable def function_field.valued_Fqt_infty (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

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

Equations