mathlib documentation

number_theory.function_field

Function fields #

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

Main definitions #

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 (polynomial Fq) (fraction_ring (polynomial Fq)) F in definitions, adding them back in lemmas when they are needed.

References #

Tags #

function field, ring of integers

def function_field (Fq F : Type) [field Fq] [field F] [algebra (fraction_ring (polynomial Fq)) F] :
Prop

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

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

theorem function_field_iff (Fq F : Type) [field Fq] [field F] (Fqt : Type u_1) [field Fqt] [algebra (polynomial Fq) Fqt] [is_fraction_ring (polynomial Fq) Fqt] [algebra (fraction_ring (polynomial Fq)) F] [algebra Fqt F] [algebra (polynomial Fq) F] [is_scalar_tower (polynomial Fq) Fqt F] [is_scalar_tower (polynomial Fq) (fraction_ring (polynomial Fq)) F] :

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

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