The discriminant budget at infinity for a plane curve

Let F be a polynomial in Y with coefficients in K[X], and suppose that every coefficient has X-degree at most a. On the infinity chart of the first projection the integral normalization of the equation is obtained by multiplying by X⁻ᵃ. Its discriminant is therefore

X⁻ᵃ⁽²ᵇ⁻²⁾ * discr(F).

The order of this element at infinity is exactly

a * (2 * b - 2) - degree(discr(F)).

This is the key complementarity needed for a Riemann--Hurwitz-free proof: the finite discriminant contribution is at most degree(discr(F)), while the above-infinity contribution is at most the displayed complementary order. In particular, one must not bound the finite and infinity contributions independently by a * (2 * b - 2).

The module also constructs the coefficientwise integral polynomial over the infinity valuation ring. Identifying a reciprocal translate of that polynomial with a primitive element of the plane-curve function field is the remaining local normalization step.

theorem BGS.CorvajaZannier.exists_local_center_eval_isUnit_of_isPrimitive_natDegree_lt_card {K A : Type u} [Field K] [CommRing A] [IsLocalRing A] [IsBezout A] [Algebra K A] (F : Polynomial A) (hF : F.IsPrimitive) (hcardK : ↑F.natDegree < Cardinal.mk K) : ∃ (c : A), IsUnit (Polynomial.eval c F)

A primitive polynomial over a local ring has a unit value at some center as soon as its degree is smaller than the cardinality of a coefficient field. The coefficient field and local ring are kept in the same universe, which is the case needed for the infinity valuation ring of K(X).

The normalized equation over K(X)

noncomputable def BGS.CorvajaZannier.infinityNormalizedPolynomial (K : Type u_1) [Field K] (a : ℕ) (F : Polynomial (Polynomial K)) : Polynomial (RatFunc K)

Multiply an equation over K[X] by X⁻ᵃ on the infinity chart of the first projection.

Equations

• BGS.CorvajaZannier.infinityNormalizedPolynomial K a F = Polynomial.C (RatFunc.X⁻¹ ^ a) * Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) F

theorem BGS.CorvajaZannier.infinityNormalizedPolynomial_natDegree (K : Type u_1) [Field K] (a : ℕ) (F : Polynomial (Polynomial K)) : (infinityNormalizedPolynomial K a F).natDegree = F.natDegree

Scaling by X⁻ᵃ does not change the degree in the second variable.

theorem BGS.CorvajaZannier.infinityNormalizedPolynomial_discr (K : Type u_1) [Field K] (a : ℕ) (F : Polynomial (Polynomial K)) : (infinityNormalizedPolynomial K a F).discr = (RatFunc.X⁻¹ ^ a) ^ (2 * F.natDegree - 2) * (algebraMap (Polynomial K) (RatFunc K)) F.discr

Exact discriminant formula for the infinity-normalized equation.

theorem BGS.CorvajaZannier.ratFuncInfinityOrder_infinityNormalizedPolynomial_discr (K : Type u_1) [Field K] (a : ℕ) (F : Polynomial (Polynomial K)) (hdiscr : F.discr ≠ 0) : ratFuncInfinityOrder (infinityNormalizedPolynomial K a F).discr = ↑(a * (2 * F.natDegree - 2)) - ↑F.discr.natDegree

The infinity order of the normalized discriminant is the complement of the finite polynomial discriminant degree in the full bidegree budget.

The normalized equation over the infinity valuation ring

theorem BGS.CorvajaZannier.infinityNormalizedCoefficient_mem (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (a : ℕ) (P : Polynomial K) (hdegree : P.natDegree ≤ a) : (RatFunc.inftyValuation K) (RatFunc.X⁻¹ ^ a * (algebraMap (Polynomial K) (RatFunc K)) P) ≤ 1

A polynomial of degree at most a, multiplied by X⁻ᵃ, is integral at infinity.

noncomputable def BGS.CorvajaZannier.infinityNormalizedCoefficient (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (a : ℕ) (P : Polynomial K) (hdegree : P.natDegree ≤ a) : ↥(RatFuncInfinityIntegers K)

The coefficient X⁻ᵃ P(X) as an element of the infinity valuation ring.

Equations

• BGS.CorvajaZannier.infinityNormalizedCoefficient K a P hdegree = ⟨RatFunc.X⁻¹ ^ a * (algebraMap (Polynomial K) (RatFunc K)) P, ⋯⟩

@[simp]

theorem BGS.CorvajaZannier.infinityNormalizedCoefficient_coe (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (a : ℕ) (P : Polynomial K) (hdegree : P.natDegree ≤ a) : ↑(infinityNormalizedCoefficient K a P hdegree) = RatFunc.X⁻¹ ^ a * (algebraMap (Polynomial K) (RatFunc K)) P

noncomputable def BGS.CorvajaZannier.infinityNormalizedIntegralPolynomial (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (a : ℕ) (F : Polynomial (Polynomial K)) (hcoeff : ∀ (i : ℕ), (F.coeff i).natDegree ≤ a) : Polynomial ↥(RatFuncInfinityIntegers K)

The coefficientwise integral infinity-chart equation.

Equations

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

theorem BGS.CorvajaZannier.infinityNormalizedIntegralPolynomial_map (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (a : ℕ) (F : Polynomial (Polynomial K)) (hcoeff : ∀ (i : ℕ), (F.coeff i).natDegree ≤ a) : Polynomial.map (algebraMap (↥(RatFuncInfinityIntegers K)) (RatFunc K)) (infinityNormalizedIntegralPolynomial K a F hcoeff) = infinityNormalizedPolynomial K a F

Extending the integral infinity-chart equation to K(X) recovers the field-valued normalization.