Weighted boundary support for a plane curve

This file proves the sharp coordinate-boundary estimate needed in the Corvaja--Zannier middle game. The exhaustive places are defined using the first-coordinate RatFunc model. To bound the positive divisor of the second coordinate, each positive place is transported to the finite chart of the second-coordinate model. The transport preserves both the normalized valuation and the residue degree; injectivity then compares the two weighted positive-divisor sums.

The final theorem is stated directly for the zero/pole boundary propositionTwoExceptionalPlaces of positive coordinate powers.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.probePolynomialAlgebra (K : Type u) [Field K] (L : Type v) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the plane curve boundary support construction.

Equations

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

theorem BGS.CorvajaZannier.probePolynomialScalarTower (K : Type u) [Field K] (L : Type v) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.probeFiniteConstantAlgebra (K : Type u) [Field K] (L : Type v) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the plane curve boundary support construction.

Equations

• BGS.CorvajaZannier.probeFiniteConstantAlgebra K L = ((algebraMap (Polynomial K) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)).comp (algebraMap K (Polynomial K))).toAlgebra

theorem BGS.CorvajaZannier.probeFiniteConstantTower (K : Type u) [Field K] (L : Type v) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.probeInfinityConstantAlgebra (K : Type u) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Algebra K ↥(RatFuncInfinityIntegers K)

The algebra structure from K to (RatFuncInfinityIntegers K) used in the plane curve boundary support construction.

Equations

• BGS.CorvajaZannier.probeInfinityConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

theorem BGS.CorvajaZannier.probeInfinityConstantTower (K : Type u) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsScalarTower K (↥(RatFuncInfinityIntegers K)) (RatFunc K)

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.probeInfinityClosureConstantAlgebra (K : Type u) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type v) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the plane curve boundary support construction.

Equations

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

theorem BGS.CorvajaZannier.probeInfinityClosureConstantTower (K : Type u) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type v) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.probeFiniteIntegralClosureIsDedekindDomain (K : Type u) [Field K] (L : Type v) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.probeFiniteIntegralClosureIsFractionRing (K : Type u) [Field K] (L : Type v) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(RatFuncFiniteIntegralClosure K L)) L

theorem BGS.CorvajaZannier.probeInfinityIntegralClosureIsDedekindDomain (K : Type u) [Field K] [DecidableEq (RatFunc K)] (L : Type v) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.probeInfinityIntegralClosureIsFractionRing (K : Type u) [Field K] [DecidableEq (RatFunc K)] (L : Type v) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(RatFuncInfinityIntegralClosure K L)) L

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_planeCurveSecondCoordinate_le_degreeOf_first {K₀ : Type u_1} [Field K₀] [Finite K₀] [DecidableEq K₀] [DecidableEq (RatFunc K₀)] {f : MvPolynomial (Fin 2) K₀} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have this := ⋯; have hx := ⋯; let this_1 := planeCurveFirstCoordinateRatFuncAlgebra f hx; have this_2 := ⋯; have this_3 := ⋯; finiteExtensionPositiveDegree K₀ (PlaneCurveFunctionField f) (planeCurveFunction f 1) ≤ MvPolynomial.degreeOf 0 f

theorem BGS.CorvajaZannier.planeCurve_propositionTwoExceptionalPlaces_weightedDegree_le {K₀ : Type u_1} [Field K₀] [Finite K₀] [DecidableEq K₀] [DecidableEq (RatFunc K₀)] {f : MvPolynomial (Fin 2) K₀} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : have this := ⋯; have hx := ⋯; let this_1 := planeCurveFirstCoordinateRatFuncAlgebra f hx; have this_2 := ⋯; have this_3 := ⋯; ∑ w ∈ propositionTwoExceptionalPlaces K₀ (PlaneCurveFunctionField f) (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n), finiteExtensionPlaceDegree K₀ (PlaneCurveFunctionField f) w ≤ 2 * (MvPolynomial.degreeOf 0 f + MvPolynomial.degreeOf 1 f)

The zero/pole boundary of positive powers of the two plane-curve coordinates has degree at most twice the sum of the two coordinate degrees.