The rational parameter's pole divisor in a finite extension

For a finite separable extension L / K(X), the image of RatFunc.X is integral at every finite place. At a place P above infinity its order is exactly -e(P), because X⁻¹ is the uniformizer of the base infinity place. Consequently its complete pole divisor is supported exactly above infinity, with coefficient e(P), and its height is [L : K(X)] by the ramification--inertia degree formula.

These statements do not require the constant field K to be finite.

@[instance_reducible]

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

The algebra structure from K[X] to L used in the rat func parameter pole construction.

Equations

• BGS.HasseWeil.ratFuncParameterPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

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

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

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

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

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

theorem BGS.HasseWeil.ratFuncParameterInfinityIntegralClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.ratFuncParameterInfinityIntegralClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.ratFuncParameterInfinityBaseTorsionFreeTop (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (↥(CorvajaZannier.RatFuncInfinityIntegers K)) L

theorem BGS.HasseWeil.ratFuncParameterInfinityIntegralClosureIsTorsionFree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.ratFuncParameterInfinityIntegralClosureIsDedekindDomain (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.ratFuncParameterInfinityIntegralClosureIsFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) L

@[instance_reducible]

noncomputable def BGS.HasseWeil.ratFuncParameterInfinityPlaceFintype (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Fintype ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)

A finite enumeration of (FiniteExtensionInfinityPlace K L) used in the rat func parameter pole construction.

Equations

• BGS.HasseWeil.ratFuncParameterInfinityPlaceFintype K L = ⋯.fintype

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_ratFuncX_inl_nonnegative (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) : 0 ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)) (Sum.inl q)

The rational parameter X is integral at every finite place.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_ratFuncX_inr_eq_neg_ramificationIdx (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : (CorvajaZannier.finiteExtensionPrincipalDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)) (Sum.inr P) = -↑((↑P).ramificationIdx ↥(CorvajaZannier.RatFuncInfinityIntegers K))

At a place P above infinity, the rational parameter has order exactly the negative ramification index.

theorem BGS.HasseWeil.finiteExtensionPoleDivisor_ratFuncX_inl_eq_zero (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) : (finiteExtensionPoleDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)) (Sum.inl q) = 0

The pole divisor of the rational parameter vanishes at finite places.

theorem BGS.HasseWeil.finiteExtensionPoleDivisor_ratFuncX_inr_eq_ramificationIdx (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : (finiteExtensionPoleDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)) (Sum.inr P) = ↑((↑P).ramificationIdx ↥(CorvajaZannier.RatFuncInfinityIntegers K))

Above infinity, the pole coefficient of the rational parameter is exactly the ramification index.

theorem BGS.HasseWeil.finiteExtensionPoleDivisor_ratFuncX_apply (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (v : CorvajaZannier.FiniteExtensionPlace K L) : (finiteExtensionPoleDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)) v = match v with | Sum.inl val => 0 | Sum.inr P => ↑((↑P).ramificationIdx ↥(CorvajaZannier.RatFuncInfinityIntegers K))

Pointwise description of the complete pole divisor of the rational parameter: it is zero at finite places and has coefficient e(P) at every place above infinity.

theorem BGS.HasseWeil.finiteExtensionPoleDivisor_ratFuncX_support (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : (finiteExtensionPoleDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)).support = Finset.map Function.Embedding.inr Finset.univ

The support of the pole divisor of the rational parameter consists exactly of the places above infinity.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_ratFuncX_negativeSupport (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : {v ∈ (CorvajaZannier.finiteExtensionPrincipalDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)).support | (CorvajaZannier.finiteExtensionPrincipalDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)) v < 0} = Finset.map Function.Embedding.inr Finset.univ

The negative support of the principal divisor of the rational parameter consists exactly of the places above infinity.

theorem BGS.HasseWeil.finiteExtensionHeight_ratFuncX_eq_finrank (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : CorvajaZannier.finiteExtensionHeight K L ((algebraMap (RatFunc K) L) RatFunc.X) = Module.finrank (RatFunc K) L

The height of the rational parameter in a finite separable extension is the extension degree.