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 Fstates thatFis a function field over the (finite) fieldFq, i.e. it is a finite extension of the field of rational functions in one variable overFq.function_field.ring_of_integersdefines the ring of integers corresponding to a function field as the integral closure ofFq[X]in the function field.function_field.infty_valuation: The place at infinity onFq(t)is the nonarchimedean valuation onFq(t)with uniformizer1/t.function_field.Fqt_infty: The completionFq((t⁻¹))ofFq(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
@[reducible]
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]
[is_fraction_ring (polynomial Fq) Fqt]
[algebra (ratfunc Fq) F]
[algebra Fqt F]
[algebra (polynomial Fq) F]
[is_scalar_tower (polynomial Fq) Fqt F]
[is_scalar_tower (polynomial Fq) (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 (polynomial Fq) F]
[algebra (ratfunc Fq) F]
[is_scalar_tower (polynomial Fq) (ratfunc Fq) F] :
function.injective ⇑(algebra_map (polynomial Fq) F)
noncomputable
def
function_field.ring_of_integers
(Fq F : Type)
[field Fq]
[field F]
[algebra (polynomial Fq) F] :
subalgebra (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
- function_field.ring_of_integers Fq F = integral_closure (polynomial Fq) F
@[protected, instance]
def
function_field.ring_of_integers.is_domain
(Fq F : Type)
[field Fq]
[field F]
[algebra (polynomial Fq) F] :
@[protected, instance]
def
function_field.ring_of_integers.is_integral_closure
(Fq F : Type)
[field Fq]
[field F]
[algebra (polynomial Fq) F] :
is_integral_closure ↥(function_field.ring_of_integers Fq F) (polynomial Fq) F
theorem
function_field.ring_of_integers.algebra_map_injective
(Fq F : Type)
[field Fq]
[field F]
[algebra (polynomial Fq) F]
[algebra (ratfunc Fq) F]
[is_scalar_tower (polynomial Fq) (ratfunc Fq) F] :
theorem
function_field.ring_of_integers.not_is_field
(Fq F : Type)
[field Fq]
[field F]
[algebra (polynomial Fq) F]
[algebra (ratfunc Fq) F]
[is_scalar_tower (polynomial Fq) (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]
[is_scalar_tower (polynomial Fq) (ratfunc Fq) F]
[function_field Fq F] :
@[protected, instance]
def
function_field.ring_of_integers.is_integrally_closed
(Fq F : Type)
[field Fq]
[field F]
[algebra (polynomial Fq) F]
[algebra (ratfunc Fq) F]
[is_scalar_tower (polynomial Fq) (ratfunc Fq) F]
[function_field Fq F] :
@[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]
[is_scalar_tower (polynomial Fq) (ratfunc Fq) F]
[function_field Fq F]
[is_separable (ratfunc Fq) F] :
is_noetherian (polynomial Fq) ↥(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 (polynomial Fq) F]
[algebra (ratfunc Fq) F]
[is_scalar_tower (polynomial Fq) (ratfunc Fq) F]
[function_field Fq F]
[is_separable (ratfunc 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) :
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)] :
theorem
function_field.infty_valuation.map_one'
(Fq : Type)
[field Fq]
[decidable_eq (ratfunc Fq)] :
theorem
function_field.infty_valuation.map_mul'
(Fq : Type)
[field Fq]
[decidable_eq (ratfunc Fq)]
(x y : ratfunc Fq) :
theorem
function_field.infty_valuation.map_add_le_max'
(Fq : Type)
[field Fq]
[decidable_eq (ratfunc Fq)]
(x y : ratfunc Fq) :
@[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)] :
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} :
@[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) :
function_field.infty_valuation_def Fq (⇑(algebra_map (polynomial Fq) (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
theorem
function_field.infty_valued_Fqt.def
(Fq : Type)
[field Fq]
[decidable_eq (ratfunc Fq)]
{x : ratfunc Fq} :
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
- function_field.Fqt_infty.field Fq = let _inst : valued (ratfunc Fq) (with_zero (multiplicative ℤ)) := function_field.infty_valued_Fqt Fq in uniform_space.completion.field
@[protected, instance]
noncomputable
def
function_field.Fqt_infty.inhabited
(Fq : Type)
[field Fq]
[decidable_eq (ratfunc 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)] :
The valuation at infinity on k(t) extends to a valuation on Fqt_infty.
Equations
theorem
function_field.valued_Fqt_infty.def
(Fq : Type)
[field Fq]
[decidable_eq (ratfunc Fq)]
{x : function_field.Fqt_infty Fq} :