mathlib documentation

number_theory.function_field

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

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

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

theorem algebra_map_injective (Fq F : Type) [field Fq] [field F] [algebra Fq[X] F] [algebra (ratfunc Fq) F] [is_scalar_tower Fq[X] (ratfunc Fq) F] :

function.injective ⇑(algebra_map Fq[X] F)

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

@[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)

@[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

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

function.injective ⇑(algebra_map Fq[X] ↥(function_field.ring_of_integers Fq F))

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

¬is_field ↥(function_field.ring_of_integers Fq F)

@[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] [is_scalar_tower Fq[X] (ratfunc Fq) F] [function_field Fq F] :

is_fraction_ring ↥(function_field.ring_of_integers Fq F) F

@[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] [is_scalar_tower Fq[X] (ratfunc Fq) F] [function_field Fq F] :

is_integrally_closed ↥(function_field.ring_of_integers Fq F)

@[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] [is_scalar_tower Fq[X] (ratfunc Fq) F] [function_field Fq F] [is_separable (ratfunc Fq) F] :

is_dedekind_domain ↥(function_field.ring_of_integers Fq F)

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) :

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

Equations

function_field.infty_valuation_def Fq r = ite (r = 0) 0 ↑(⇑multiplicative.of_add r.int_degree)

theorem function_field.infty_valuation.map_zero' (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

function_field.infty_valuation_def Fq 0 = 0

theorem function_field.infty_valuation.map_one' (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

function_field.infty_valuation_def Fq 1 = 1

theorem function_field.infty_valuation.map_mul' (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] (x y : ratfunc Fq) :

function_field.infty_valuation_def Fq (x * y) = (function_field.infty_valuation_def Fq x) * function_field.infty_valuation_def Fq y

theorem function_field.infty_valuation.map_add_le_max' (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] (x y : ratfunc Fq) :

function_field.infty_valuation_def Fq (x + y) ≤ max (function_field.infty_valuation_def Fq x) (function_field.infty_valuation_def Fq y)

@[simp]

theorem function_field.infty_valuation_of_nonzero (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {x : ratfunc Fq} (hx : x ≠ 0) :

function_field.infty_valuation_def Fq x = ↑(⇑multiplicative.of_add x.int_degree)

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

valuation (ratfunc Fq) (with_zero (multiplicative ℤ))

The valuation at infinity on Fq(t).

Equations

function_field.infty_valuation Fq = {to_monoid_with_zero_hom := {to_fun := function_field.infty_valuation_def Fq (λ (a b : ratfunc Fq), _inst_3 a b), map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}

@[simp]

theorem function_field.infty_valuation_apply (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {x : ratfunc Fq} :

⇑(function_field.infty_valuation Fq) x = function_field.infty_valuation_def Fq x

@[simp]

theorem function_field.infty_valuation.C (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {k : Fq} (hk : k ≠ 0) :

function_field.infty_valuation_def Fq (⇑ratfunc.C k) = ↑(⇑multiplicative.of_add 0)

@[simp]

theorem function_field.infty_valuation.X (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

function_field.infty_valuation_def Fq ratfunc.X = ↑(⇑multiplicative.of_add 1)

@[simp]

theorem function_field.infty_valuation.polynomial (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {p : Fq[X]} (hp : p ≠ 0) :

function_field.infty_valuation_def Fq (⇑(algebra_map Fq[X] (ratfunc Fq)) p) = ↑(⇑multiplicative.of_add ↑(p.nat_degree))

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

valued (ratfunc Fq) (with_zero (multiplicative ℤ))

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

Equations

function_field.infty_valued_Fqt Fq = {v := function_field.infty_valuation Fq (λ (a b : ratfunc Fq), _inst_3 a b)}

theorem function_field.infty_valued_Fqt.def (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {x : ratfunc Fq} :

⇑valued.v x = function_field.infty_valuation_def Fq x

noncomputable def function_field.infty_valued_Fqt.topological_space (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

topological_space (ratfunc Fq)

The topology structure on Fq(t) induced by the valuation at infinity.

Equations

function_field.infty_valued_Fqt.topological_space Fq = valued.topological_space (with_zero (multiplicative ℤ))

theorem function_field.infty_valued_Fqt.topological_division_ring (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

topological_division_ring (ratfunc Fq)

noncomputable def function_field.infty_valued_Fqt.uniform_space (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

uniform_space (ratfunc Fq)

The uniform structure on k(t) induced by the valuation at infinity.

Equations

function_field.infty_valued_Fqt.uniform_space Fq = topological_add_group.to_uniform_space (ratfunc Fq)

theorem function_field.infty_valued_Fqt.uniform_add_group (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

uniform_add_group (ratfunc Fq)

theorem function_field.infty_valued_Fqt.completable_top_field (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

completable_top_field (ratfunc Fq)

theorem function_field.infty_valued_Fqt.separated_space (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

separated_space (ratfunc Fq)

def function_field.Fqt_infty (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

Type

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

Equations

function_field.Fqt_infty Fq = uniform_space.completion (ratfunc Fq)

@[protected, instance]

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

field (function_field.Fqt_infty Fq)

Equations

function_field.Fqt_infty.field Fq = field_completion

@[protected, instance]

noncomputable def function_field.Fqt_infty.inhabited (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

inhabited (function_field.Fqt_infty Fq)

Equations

function_field.Fqt_infty.inhabited Fq = {default := 0}

@[protected, instance]

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

valued (function_field.Fqt_infty Fq) (with_zero (multiplicative ℤ))

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

Equations

function_field.valued_Fqt_infty Fq = {v := valued.extension_valuation (function_field.infty_valued_Fqt Fq)}

theorem function_field.valued_Fqt_infty.def (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] {x : function_field.Fqt_infty Fq} :

⇑valued.v x = valued.extension x

@[protected, instance]

noncomputable def function_field.Fqt_infty.topological_space (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

topological_space (function_field.Fqt_infty Fq)

Equations

function_field.Fqt_infty.topological_space Fq = valued.topological_space (with_zero (multiplicative ℤ))

@[protected, instance]

def function_field.Fqt_infty.topological_division_ring (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

topological_division_ring (function_field.Fqt_infty Fq)

@[protected, instance]

def function_field.Fqt_infty.topological_ring (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

topological_ring (function_field.Fqt_infty Fq)

@[protected, instance]

def function_field.Fqt_infty.topological_add_group (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

topological_add_group (function_field.Fqt_infty Fq)

@[protected, instance]

noncomputable def function_field.Fqt_infty.uniform_space (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

uniform_space (function_field.Fqt_infty Fq)

Equations

function_field.Fqt_infty.uniform_space Fq = topological_add_group.to_uniform_space (function_field.Fqt_infty Fq)

@[protected, instance]

def function_field.Fqt_infty.uniform_add_group (Fq : Type) [field Fq] [decidable_eq (ratfunc Fq)] :

uniform_add_group (function_field.Fqt_infty Fq)