The complementary different bound above infinity #
For a primitive infinity-chart equation of bidegree at most (a,b), the
weighted different contribution above infinity is bounded by
a * (2 * b - 2) - degree(discriminant).
Together with the finite-place discriminant bound, this gives the sharp total different budget used in the Corvaja--Zannier plane-curve estimate.
@[instance_reducible]
noncomputable def
BGS.CorvajaZannier.infinityComplementConstantAlgebra
(K : Type u_1)
[Field K]
[DecidableEq K]
[DecidableEq (RatFunc K)]
:
Algebra K ↥(RatFuncInfinityIntegers K)
The algebra structure from K to (RatFuncInfinityIntegers K) used in the plane curve
infinity complement construction.
Equations
Instances For
theorem
BGS.CorvajaZannier.infinityComplementConstantTower
(K : Type u_1)
[Field K]
[DecidableEq K]
[DecidableEq (RatFunc K)]
:
IsScalarTower K (↥(RatFuncInfinityIntegers K)) (RatFunc K)
theorem
BGS.CorvajaZannier.infinityComplementTopIsTorsionFree
(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]
:
theorem
BGS.CorvajaZannier.planeCurveInfinityDifferentDegree_le_bidegreeComplement
(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]
(a : ℕ)
(F : Polynomial (Polynomial K))
(hcoeff : ∀ (i : ℕ), (F.coeff i).natDegree ≤ a)
(i : ℕ)
(hFi : F.coeff i ≠ 0)
(hi : (F.coeff i).natDegree = a)
(v : L)
(hv : (Polynomial.aeval v) (infinityNormalizedIntegralPolynomial K a F hcoeff) = 0)
(hprimitive : (RatFunc K)[v] = ⊤)
(hdegree : F.natDegree = Module.finrank (RatFunc K) L)
(hFdiscr : F.discr ≠ 0)
(hcard : ↑F.natDegree < Cardinal.mk K)
:
The residue-degree-weighted different above infinity is bounded by the complement of the finite discriminant degree in the full bidegree budget.