Documentation

Mathlib.NumberTheory.FunctionField

Function fields #

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

Main definitions #

FunctionField F K states that K is a function field over the field F, i.e. it is a finite extension of the field of rational functions in one variable over F.
FunctionField.ringOfIntegers defines the ring of integers corresponding to a function field as the integral closure of F[X] 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 IsScalarTower F[X] (FractionRing F[X]) K in definitions, adding them back in lemmas when they are needed.

References #

[D. Marcus, Number Fields][marcus1977number]
[J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory][cassels1967algebraic]
[P. Samuel, Algebraic Theory of Numbers][samuel1967]

Tags #

function field, ring of integers

@[reducible, inline]

abbrev FunctionField (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (RatFunc F) K] :

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

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

Equations

FunctionField F K = FiniteDimensional (RatFunc F) K

Instances For

theorem functionField_iff (F : Type u_1) (K : Type u_2) [Field F] [Field K] (Ft : Type u_3) [Field Ft] [Algebra (Polynomial F) Ft] [IsFractionRing (Polynomial F) Ft] [Algebra (RatFunc F) K] [Algebra Ft K] [Algebra (Polynomial F) K] [IsScalarTower (Polynomial F) Ft K] [IsScalarTower (Polynomial F) (RatFunc F) K] :

FunctionField F K ↔ FiniteDimensional Ft K

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

theorem FunctionField.algebraMap_injective (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] :

Function.Injective ⇑(algebraMap (Polynomial F) K)

noncomputable def FunctionField.ringOfIntegers (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] :

Subalgebra (Polynomial F) K

The function field analogue of NumberField.ringOfIntegers: FunctionField.ringOfIntegers F K is the integral closure of F[X] in K.

We don't actually assume K is a function field over F in the definition, only when proving its properties.

Equations

FunctionField.ringOfIntegers F K = integralClosure (Polynomial F) K

Instances For

instance FunctionField.ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomial (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] :

IsDomain ↥(ringOfIntegers F K)

instance FunctionField.ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomial (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] :

IsIntegralClosure (↥(ringOfIntegers F K)) (Polynomial F) K

theorem FunctionField.ringOfIntegers.algebraMap_injective (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] :

Function.Injective ⇑(algebraMap (Polynomial F) ↥(ringOfIntegers F K))

theorem FunctionField.ringOfIntegers.not_isField (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] :

¬IsField ↥(ringOfIntegers F K)

instance FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomial (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] [FunctionField F K] :

IsFractionRing (↥(ringOfIntegers F K)) K

instance FunctionField.ringOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] [FunctionField F K] :

IsIntegrallyClosed ↥(ringOfIntegers F K)

instance FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] [FunctionField F K] [Algebra.IsSeparable (RatFunc F) K] :

IsNoetherian (Polynomial F) ↥(ringOfIntegers F K)

instance FunctionField.ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] [FunctionField F K] [Algebra.IsSeparable (RatFunc F) K] :

IsDedekindDomain ↥(ringOfIntegers F K)

@[deprecated RatFunc.inftyValuationDef (since := "2026-04-14")]

def FunctionField.inftyValuationDef (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (r : RatFunc F) :

WithZero (Multiplicative ℤ)

Alias of RatFunc.inftyValuationDef.

Equations

FunctionField.inftyValuationDef = RatFunc.inftyValuationDef

Instances For

@[deprecated RatFunc.InftyValuation.map_zero' (since := "2026-04-14")]

theorem FunctionField.InftyValuation.map_zero' (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] :

RatFunc.inftyValuationDef F 0 = 0

Alias of RatFunc.InftyValuation.map_zero'.

@[deprecated RatFunc.InftyValuation.map_one' (since := "2026-04-14")]

theorem FunctionField.InftyValuation.map_one' (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] :

RatFunc.inftyValuationDef F 1 = 1

Alias of RatFunc.InftyValuation.map_one'.

@[deprecated RatFunc.InftyValuation.map_mul' (since := "2026-04-14")]

theorem FunctionField.InftyValuation.map_mul' (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (x y : RatFunc F) :

RatFunc.inftyValuationDef F (x * y) = RatFunc.inftyValuationDef F x * RatFunc.inftyValuationDef F y

Alias of RatFunc.InftyValuation.map_mul'.

@[deprecated RatFunc.InftyValuation.map_add_le_max' (since := "2026-04-14")]

theorem FunctionField.InftyValuation.map_add_le_max' (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (x y : RatFunc F) :

RatFunc.inftyValuationDef F (x + y) ≤ max (RatFunc.inftyValuationDef F x) (RatFunc.inftyValuationDef F y)

Alias of RatFunc.InftyValuation.map_add_le_max'.

@[deprecated RatFunc.inftyValuation_of_nonzero (since := "2026-04-14")]

theorem FunctionField.inftyValuation_of_nonzero (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : RatFunc F} (hx : x ≠ 0) :

RatFunc.inftyValuationDef F x = WithZero.exp x.intDegree

Alias of RatFunc.inftyValuation_of_nonzero.

@[deprecated RatFunc.inftyValuation (since := "2026-04-14")]

def FunctionField.inftyValuation (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] :

Valuation (RatFunc F) (WithZero (Multiplicative ℤ))

Alias of RatFunc.inftyValuation.

Equations

FunctionField.inftyValuation = RatFunc.inftyValuation

Instances For

@[deprecated RatFunc.inftyValuation_apply (since := "2026-04-14")]

theorem FunctionField.inftyValuation_apply (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : RatFunc F} :

(RatFunc.inftyValuation F) x = RatFunc.inftyValuationDef F x

Alias of RatFunc.inftyValuation_apply.

@[deprecated RatFunc.inftyValuation.C (since := "2026-04-14")]

theorem FunctionField.inftyValuation.C (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {k : F} (hk : k ≠ 0) :

(RatFunc.inftyValuation F) (RatFunc.C k) = 1

Alias of RatFunc.inftyValuation.C.

@[deprecated RatFunc.inftyValuation.X (since := "2026-04-14")]

theorem FunctionField.inftyValuation.X (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] :

(RatFunc.inftyValuation F) RatFunc.X = WithZero.exp 1

Alias of RatFunc.inftyValuation.X.

@[deprecated RatFunc.inftyValuation.X_zpow (since := "2026-04-14")]

theorem FunctionField.inftyValuation.X_zpow (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (m : ℤ) :

(RatFunc.inftyValuation F) (RatFunc.X ^ m) = WithZero.exp m

Alias of RatFunc.inftyValuation.X_zpow.

@[deprecated RatFunc.inftyValuation.X_inv (since := "2026-04-14")]

theorem FunctionField.inftyValuation.X_inv (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] :

(RatFunc.inftyValuation F) (1 / RatFunc.X) = WithZero.exp (-1)

Alias of RatFunc.inftyValuation.X_inv.

@[deprecated RatFunc.inftyValuation.polynomial (since := "2026-04-14")]

theorem FunctionField.inftyValuation.polynomial (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {p : Polynomial F} (hp : p ≠ 0) :

RatFunc.inftyValuationDef F ((algebraMap (Polynomial F) (RatFunc F)) p) = WithZero.exp ↑p.natDegree

Alias of RatFunc.inftyValuation.polynomial.

@[deprecated RatFunc.inftyValued (since := "2026-04-14")]

def FunctionField.inftyValuedFt (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] :

Valued (RatFunc F) (WithZero (Multiplicative ℤ))

Alias of RatFunc.inftyValued.

Equations

FunctionField.inftyValuedFt = RatFunc.inftyValued

Instances For

@[deprecated RatFunc.inftyValued.def (since := "2026-04-14")]

theorem FunctionField.inftyValuedFt.def (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : RatFunc F} :

Valued.v x = RatFunc.inftyValuationDef F x

Alias of RatFunc.inftyValued.def.

@[deprecated RatFunc.CompletionAtInfty (since := "2026-04-14")]

def FunctionField.FtInfty (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] :

Type u_1

Alias of RatFunc.CompletionAtInfty.

Equations

FunctionField.FtInfty = RatFunc.CompletionAtInfty

Instances For

@[implicit_reducible, deprecated "Use the anonymous `Valued` instance on `RatFunc.CompletionAtInfty`" (since := "2026-04-14")]

noncomputable instance FunctionField.valuedFtInfty (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] :

Valued (RatFunc.CompletionAtInfty F) (WithZero (Multiplicative ℤ))

Equations

FunctionField.valuedFtInfty F = inferInstance

@[deprecated RatFunc.valuedCompletionAtInfty.def (since := "2026-04-14")]

theorem FunctionField.valuedFtInfty.def (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : RatFunc.CompletionAtInfty F} :

Valued.v x = Valued.extensionValuation x

Alias of RatFunc.valuedCompletionAtInfty.def.

instance FunctionField.FiniteDimensional.adjoin_X {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra (RatFunc F) K] [FunctionField F K] :

FiniteDimensional (↥F⟮RatFunc.X⟯) K

theorem FunctionField.FiniteDimensional.adjoin_algebraMap_X {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra (RatFunc F) K] [FunctionField F K] [Algebra F K] [IsScalarTower F (RatFunc F) K] :

FiniteDimensional (↥F⟮(algebraMap (RatFunc F) K) RatFunc.X⟯) K

theorem FunctionField.Algebra.IsAlgebraic.adjoin_algebraMap_X {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra (RatFunc F) K] [FunctionField F K] [Algebra F K] [IsScalarTower F (RatFunc F) K] :

Algebra.IsAlgebraic (↥F⟮(algebraMap (RatFunc F) K) RatFunc.X⟯) K

theorem FunctionField.isAlgebraic_X_over_adjoin_transcendental {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra (RatFunc F) K] [FunctionField F K] [Algebra F K] [IsScalarTower F (RatFunc F) K] {y : K} (hy : Transcendental F y) :

IsAlgebraic (↥F⟮y⟯) ((algebraMap (RatFunc F) K) RatFunc.X)

theorem FunctionField.finiteDimensional_of_adjoin_transcendental {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra (RatFunc F) K] [FunctionField F K] [Algebra F K] [IsScalarTower F (RatFunc F) K] {y : K} (hy : Transcendental F y) :

FiniteDimensional (↥F⟮y⟯) K