Function fields #

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 polynomial Fq in the function field.

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.

References #

D. Marcus, Number Fields
J.W.S. Cassels, A. Frölich, Algebraic Number Theory
[P. Samuel, Algebraic Theory of Numbers][samuel1970algebraic]

Tags #

function field, ring of integers

source

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.

source

@[protected]

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

function_field Fq F ↔ finite_dimensional Fqt F

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

source

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

subalgebra Fq[X] 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

function_field.ring_of_integers Fq F = integral_closure Fq[X] F

source

@[protected, instance]

def function_field.ring_of_integers.is_domain (Fq F : Type) [field Fq] [field F] [algebra Fq[X] F] :

is_domain ↥(function_field.ring_of_integers Fq F)

source

@[protected, instance]

def function_field.ring_of_integers.is_integral_closure (Fq F : Type) [field Fq] [field F] [algebra Fq[X] F] :

is_integral_closure ↥(function_field.ring_of_integers Fq F) Fq[X] F

source

@[protected, instance]

def function_field.ring_of_integers.is_fraction_ring (Fq F : Type) [field Fq] [field F] [algebra Fq[X] F] [algebra (ratfunc Fq) F] [function_field Fq F] [is_scalar_tower Fq[X] (ratfunc Fq) F] :

is_fraction_ring ↥(function_field.ring_of_integers Fq F) F

source

@[protected, instance]

def function_field.ring_of_integers.is_integrally_closed (Fq F : Type) [field Fq] [field F] [algebra Fq[X] F] [algebra (ratfunc Fq) F] [function_field Fq F] [is_scalar_tower Fq[X] (ratfunc Fq) F] :

is_integrally_closed ↥(function_field.ring_of_integers Fq F)

source

@[protected, instance]

def function_field.ring_of_integers.is_dedekind_domain (Fq F : Type) [field Fq] [field F] [algebra Fq[X] F] [algebra (ratfunc Fq) F] [function_field Fq F] [is_scalar_tower Fq[X] (ratfunc Fq) F] [is_separable (ratfunc Fq) F] :

is_dedekind_domain ↥(function_field.ring_of_integers Fq F)