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.
• FunctionField.inftyValuation : The place at infinity on F(t) is the nonarchimedean valuation on F(t) with uniformizer 1/t.
• FunctionField.FqtInfty : The completion F((t⁻¹)) of F(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 IsScalarTower F[X] (FractionRing F[X]) K in definitions, adding them back in lemmas when they are needed.

References

• D. Marcus, Number Fields
• J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory
• P. Samuel, Algebraic Theory of Numbers

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] : Prop

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

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

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)

The place at infinity on F(t)

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

The valuation at infinity is the nonarchimedean valuation on F(t) with uniformizer 1/t. Explicitly, if f/g ∈ F(t) is a nonzero quotient of polynomials, its valuation at infinity is exp (degree(f) - degree(g)).

Equations

• FunctionField.inftyValuationDef F r = if r = 0 then 0 else WithZero.exp r.intDegree

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

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

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

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

@[simp]

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

noncomputable def FunctionField.inftyValuation (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Valuation (RatFunc F) (WithZero (Multiplicative ℤ))

The valuation at infinity on F(t).

Equations

• FunctionField.inftyValuation F = { toFun := FunctionField.inftyValuationDef F, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

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

@[simp]

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

@[simp]

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

theorem FunctionField.inftyValuation.X_zpow (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (m : ℤ) : (inftyValuation F) (RatFunc.X ^ m) = WithZero.exp m

theorem FunctionField.inftyValuation.X_inv (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : (inftyValuation F) (1 / RatFunc.X) = WithZero.exp (-1)

theorem FunctionField.inftyValuation.polynomial (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {p : Polynomial F} (hp : p ≠ 0) : inftyValuationDef F ((algebraMap (Polynomial F) (RatFunc F)) p) = WithZero.exp ↑p.natDegree

instance FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : (inftyValuation F).IsNontrivial

instance FunctionField.instIsTrivialOnWithZeroMultiplicativeIntRatFuncInftyValuation (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Valuation.IsTrivialOn F (inftyValuation F)

@[implicit_reducible]

noncomputable def FunctionField.inftyValuedFqt (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Valued (RatFunc F) (WithZero (Multiplicative ℤ))

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

Equations

• FunctionField.inftyValuedFqt F = Valued.mk' (FunctionField.inftyValuation F)

theorem FunctionField.inftyValuedFqt.def (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : RatFunc F} : Valued.v x = inftyValuationDef F x

@[implicit_reducible]

noncomputable def FunctionField.FqtInfty.instUniformSpaceRatFunc (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : UniformSpace (RatFunc F)

The uniform space structure on RatFunc F coming from the valuation at infinity.

Equations

• FunctionField.FqtInfty.instUniformSpaceRatFunc F = (FunctionField.inftyValuedFqt F).toUniformSpace

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

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

Equations

• FunctionField.FqtInfty F = UniformSpace.Completion (RatFunc F)

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance FunctionField.FqtInfty.instAlgebraRatFunc (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Algebra (RatFunc F) (FqtInfty F)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance FunctionField.FqtInfty.instCoeRatFunc (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Coe (RatFunc F) (FqtInfty F)

Equations

• FunctionField.FqtInfty.instCoeRatFunc F = { coe := FunctionField.FqtInfty.instCoeRatFunc._aux_1 F }

@[implicit_reducible]

noncomputable instance FunctionField.FqtInfty.instInhabited (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Inhabited (FqtInfty F)

Equations

• FunctionField.FqtInfty.instInhabited F = { default := FunctionField.FqtInfty.instInhabited._aux_1 F }

@[implicit_reducible]

noncomputable instance FunctionField.valuedFqtInfty (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Valued (FqtInfty F) (WithZero (Multiplicative ℤ))

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

Equations

• FunctionField.valuedFqtInfty F = Valued.valuedCompletion

theorem FunctionField.valuedFqtInfty.def (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : FqtInfty F} : Valued.v x = Valued.extensionValuation x