Height of a polynomial in a finite rational-function extension

For a nonzero polynomial P : K[X], regarded first as a rational function and then as an element of a finite separable extension L / K(X), this file proves that the positive degree of its exhaustive principal divisor is

Module.finrank (RatFunc K) L * P.natDegree.

The proof is place-theoretic. At finite places the lift is integral, hence has nonnegative order. Above infinity its inverse is integral, hence its order is nonpositive. The positive part is therefore exactly the finite-place degree sum, which is evaluated by the norm and the rational-function product formula. No algebraic-closedness hypothesis on the constant field is needed.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.polynomialHeightPolynomialAlgebra (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 finite extension polynomial height construction.

Equations

• BGS.CorvajaZannier.polynomialHeightPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

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

theorem BGS.CorvajaZannier.polynomialHeightFiniteIntegralClosureModuleFinite (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) ↥(RatFuncFiniteIntegralClosure K L)

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

theorem BGS.CorvajaZannier.polynomialHeightPolynomialTorsionFreeTop (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.CorvajaZannier.polynomialHeightFiniteIntegralClosureIsTorsionFree (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) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.polynomialHeightInfinityIntegralClosureModuleFinite (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 ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.polynomialHeightInfinityIntegralClosureIsDedekindDomain (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 ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.finitePlaceOrder_inv_eq_neg {R : Type u_3} {F : Type u_4} [CommRing R] [IsDedekindDomain R] [Field F] [Algebra R F] [IsFractionRing R F] (v : IsDedekindDomain.HeightOneSpectrum R) (x : F) (hx : x ≠ 0) : finitePlaceOrder v x⁻¹ = -finitePlaceOrder v x

The order of an inverse at a height-one place is the negative order.

theorem BGS.CorvajaZannier.finitePlaceOrder_algebraMap_nonnegative {R : Type u_3} {F : Type u_4} [CommRing R] [IsDedekindDomain R] [Field F] [Algebra R F] [IsFractionRing R F] (v : IsDedekindDomain.HeightOneSpectrum R) (a : R) (ha : a ≠ 0) : 0 ≤ finitePlaceOrder v ((algebraMap R F) a)

A nonzero regular element has nonnegative finite-place order.

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_polynomial_cast (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] (P : Polynomial K) (hP : P ≠ 0) : ↑(finiteExtensionPositiveDegree K L ((algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) P))) = finiteExtensionFiniteDirectDegreeSum K L ((algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) P))

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_polynomial (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] (P : Polynomial K) (hP : P ≠ 0) : finiteExtensionPositiveDegree K L ((algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) P)) = Module.finrank (RatFunc K) L * P.natDegree