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
• J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory
• P. Samuel, Algebraic Theory of Numbers
• M. Rosen, Number Theory in Function Fields

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)

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

theorem FunctionField.finiteDimensional_ratFunc_of_constantExtension {F : Type u_1} (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [FaithfulSMul (Polynomial F) K] [FunctionField F K] {E : Type u_3} [Field E] [Algebra F E] [Algebra (Polynomial E) K] [FaithfulSMul (Polynomial E) K] [IsScalarTower (Polynomial F) (Polynomial E) K] : FiniteDimensional (RatFunc F) (RatFunc E)

theorem FunctionField.finiteDimensional_of_constantExtension {F : Type u_1} (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [FaithfulSMul (Polynomial F) K] [FunctionField F K] {E : Type u_3} [Field E] [Algebra F E] [Algebra (Polynomial E) K] [FaithfulSMul (Polynomial E) K] [IsScalarTower (Polynomial F) (Polynomial E) K] [Algebra.IsAlgebraic F E] : FiniteDimensional F E

Let K be a function field over F. If E is an algebraic extension of F which is contained in K then it is finite over F.

instance FunctionField.instFiniteDimensionalRatFuncSubtypeMemIntermediateField {F : Type u_1} (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [FaithfulSMul (Polynomial F) K] [FunctionField F K] [Algebra F K] (E : IntermediateField F K) [Algebra (Polynomial ↥E) K] [FaithfulSMul (Polynomial ↥E) K] [IsScalarTower (Polynomial F) (Polynomial ↥E) K] : FiniteDimensional (RatFunc F) (RatFunc ↥E)

instance FunctionField.instFiniteDimensionalSubtypeMemIntermediateFieldOfIsAlgebraic {F : Type u_1} (K : Type u_2) [Field F] [Field K] [Algebra (Polynomial F) K] [FaithfulSMul (Polynomial F) K] [FunctionField F K] [Algebra F K] (E : IntermediateField F K) [Algebra (Polynomial ↥E) K] [FaithfulSMul (Polynomial ↥E) K] [IsScalarTower (Polynomial F) (Polynomial ↥E) K] [Algebra.IsAlgebraic F ↥E] : FiniteDimensional F ↥E

Let K be a function field over F. If E is an algebraic extension of F which is contained in K then it is finite over F.