The algebraic constant field of a finite function field

For a finite separable extension N / K(t), define its algebraic constant field to be the relative algebraic closure of K in N. When K is finite, this constant field is finite-dimensional over K.

The finiteness proof is place-theoretic. Algebraic constants are integral over K[X], hence map into the finite integral closure. Reduction modulo any height-one prime is injective on the constant field, because it is a field. Choosing a prime above (X) embeds the constants into a finite quotient.

@[instance_reducible]

noncomputable def BGS.HasseWeil.functionFieldConstantAlgebra (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : Algebra K N

The algebra structure from K to N used in the function field constant field construction.

Equations

• BGS.HasseWeil.functionFieldConstantAlgebra K N = ((algebraMap (RatFunc K) N).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.functionFieldConstantRatFuncTower (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : IsScalarTower K (RatFunc K) N

@[instance_reducible]

noncomputable def BGS.HasseWeil.functionFieldConstantPolynomialAlgebra (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : Algebra (Polynomial K) N

The algebra structure from K[X] to N used in the function field constant field construction.

Equations

• BGS.HasseWeil.functionFieldConstantPolynomialAlgebra K N = ((algebraMap (RatFunc K) N).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.functionFieldConstantPolynomialRatFuncTower (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : IsScalarTower (Polynomial K) (RatFunc K) N

theorem BGS.HasseWeil.functionFieldConstantPolynomialTower (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : IsScalarTower K (Polynomial K) N

theorem BGS.HasseWeil.functionFieldConstantPolynomialTorsionFreeTop (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] : Module.IsTorsionFree (Polynomial K) N

@[instance_reducible]

noncomputable def BGS.HasseWeil.functionFieldConstantFiniteClosureAlgebra (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K N)

The algebra structure from K to (RatFuncFiniteIntegralClosure K N) used in the function field constant field construction.

Equations

• BGS.HasseWeil.functionFieldConstantFiniteClosureAlgebra K N = ((algebraMap (Polynomial K) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K N)).comp (algebraMap K (Polynomial K))).toAlgebra

theorem BGS.HasseWeil.functionFieldConstantFiniteClosureTower (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : IsScalarTower K (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K N)

theorem BGS.HasseWeil.functionFieldConstantFiniteClosureModuleFinite (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [FiniteDimensional (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K N)

theorem BGS.HasseWeil.functionFieldConstantFiniteClosureIntegral (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : Algebra.IsIntegral (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K N)

theorem BGS.HasseWeil.functionFieldConstantFiniteClosureTorsionFree (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] : Module.IsTorsionFree (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K N)

theorem BGS.HasseWeil.functionFieldConstantFiniteClosureDedekind (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [FiniteDimensional (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] : IsDedekindDomain ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K N)

@[reducible, inline]

noncomputable abbrev BGS.HasseWeil.FunctionFieldConstantField (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : IntermediateField K N

The algebraic constant field of N / K(t).

Equations

• BGS.HasseWeil.FunctionFieldConstantField K N = algebraicClosure K N

def BGS.HasseWeil.functionFieldConstantToFiniteIntegralClosure (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] : ↥(FunctionFieldConstantField K N) →ₐ[K] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K N)

Algebraic constants are integral over the finite polynomial model.

Equations

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

theorem BGS.HasseWeil.functionFieldConstantFinitePlaceMaximal (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [FiniteDimensional (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] (Q : CorvajaZannier.FiniteExtensionFinitePlace K N) : Q.asIdeal.IsMaximal

noncomputable def BGS.HasseWeil.functionFieldConstantQuotientAlgHom (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] (Q : CorvajaZannier.FiniteExtensionFinitePlace K N) : ↥(FunctionFieldConstantField K N) →ₐ[K] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K N) ⧸ Q.asIdeal

Reduction modulo a finite place, restricted to the algebraic constant field.

Equations

• BGS.HasseWeil.functionFieldConstantQuotientAlgHom K N Q = (Ideal.Quotient.mkₐ K Q.asIdeal).comp (BGS.HasseWeil.functionFieldConstantToFiniteIntegralClosure K N)

theorem BGS.HasseWeil.functionFieldConstantQuotientAlgHom_injective (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] (Q : CorvajaZannier.FiniteExtensionFinitePlace K N) : Function.Injective ⇑(functionFieldConstantQuotientAlgHom K N Q)

Reduction at a finite place is injective on algebraic constants.

theorem BGS.HasseWeil.ratFuncFinitePlaceResidueField_finite (K : Type u_1) [Field K] [Finite K] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : Finite p.asIdeal.ResidueField

The residue field of a rational-function finite place is finite over a finite constant field.

theorem BGS.HasseWeil.finiteExtensionFinitePlaceResidueField_finite (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [FiniteDimensional (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] [Finite K] (P : CorvajaZannier.FiniteExtensionFinitePlace K N) : Finite P.asIdeal.ResidueField

Every finite-place residue field of a finite separable function field is finite over a finite constant field.

instance BGS.HasseWeil.functionFieldConstantField_finiteDimensional (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [FiniteDimensional (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] [Finite K] : FiniteDimensional K ↥(FunctionFieldConstantField K N)

Over a finite base field, the algebraic constant field of a finite separable function field is finite-dimensional.

instance BGS.HasseWeil.functionFieldConstantField_finite (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [FiniteDimensional (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] [Finite K] : Finite ↥(FunctionFieldConstantField K N)

The algebraic constant field is a finite type when the original constants are finite.

instance BGS.HasseWeil.functionFieldConstantField_isGalois (K : Type u_1) (N : Type u_2) [Field K] [Field N] [Algebra (RatFunc K) N] [FiniteDimensional (RatFunc K) N] [Algebra.IsSeparable (RatFunc K) N] [Finite K] : IsGalois K ↥(FunctionFieldConstantField K N)

The algebraic constant field is Galois over the finite base field.