Rational normalization places and affine exceptional fibers

This file begins the reverse comparison from degree-one normalization places to affine rational points. It supplies the two finite-place counting APIs needed independently of the remaining local-center argument:

• degree-one finite places of K(X) are canonically equivalent to K;
• rational finite places whose base coordinate is a zero of a polynomial R are bounded by #Z(R) times the function-field degree.

For a plane equation, the exceptional base polynomial is the product of the second-coordinate leading coefficient and the derivative resultant. The leading-coefficient factor is necessary: the derivative resultant alone need not detect degree drop after specialization, especially in positive characteristic.

noncomputable def BGS.HasseWeil.linearNormalizedPrime (K : Type u_1) [Field K] [DecidableEq K] (a : K) : CorvajaZannier.NormalizedPrimePolynomial K

The normalized prime polynomial corresponding to the affine coordinate a.

Equations

• BGS.HasseWeil.linearNormalizedPrime K a = ⟨Polynomial.X - Polynomial.C a, ⋯⟩

noncomputable def BGS.HasseWeil.ratFuncRationalFinitePlaceEquiv (K : Type u_1) [Field K] [DecidableEq K] : RatFuncRationalFinitePlace K ≃ K

Degree-one finite places of K(X) are exactly the linear primes X - a, hence are canonically parametrized by a : K.

Equations

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

noncomputable def BGS.HasseWeil.secondCoordinateAffineExceptionalPolynomial {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Polynomial K

The base polynomial containing both the critical fibers and the fibers where the second-coordinate degree drops.

Equations

• BGS.HasseWeil.secondCoordinateAffineExceptionalPolynomial f = (BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate f).leadingCoeff * BGS.HasseWeil.secondCoordinateCriticalResultant f

theorem BGS.HasseWeil.secondCoordinateAffineExceptionalPolynomial_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : secondCoordinateAffineExceptionalPolynomial f ≠ 0

theorem BGS.HasseWeil.secondCoordinateAffineExceptionalPolynomial_natDegree_le {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) : (secondCoordinateAffineExceptionalPolynomial f).natDegree ≤ firstDegree + (2 * secondDegree - 1) * firstDegree

theorem BGS.HasseWeil.secondCoordinateAffineExceptionalBase_card_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : Fintype.card { a : K // Polynomial.eval a (secondCoordinateAffineExceptionalPolynomial f) = 0 } ≤ firstDegree + (2 * secondDegree - 1) * firstDegree

@[instance_reducible]

noncomputable def BGS.HasseWeil.rationalComparisonPolynomialAlgebra (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 plane rational place affine comparison construction.

Equations

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

theorem BGS.HasseWeil.rationalComparisonPolynomialScalarTower (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.rationalComparisonFiniteClosureModuleFinite (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.rationalComparisonPolynomialTorsionFreeTop (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.rationalComparisonFiniteClosureTorsionFree (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.rationalComparisonFiniteClosureNoZeroSMulDivisors (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] : NoZeroSMulDivisors (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.rationalComparisonFiniteClosureDedekind (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] : IsDedekindDomain ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

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

@[instance_reducible]

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

The algebra structure from K to L used in the plane rational place affine comparison construction.

Equations

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

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.rationalComparisonFiniteClosureConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the plane rational place affine comparison construction.

Equations

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

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

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

theorem BGS.HasseWeil.exists_constant_sub_finitePlaceOrder_pos_of_nonnegative (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] (q : FiniteExtensionRationalFinitePlace K L) (z : L) (hz : z ≠ 0) (hnotConstant : ∀ (c : K), z ≠ (algebraMap K L) c) (hregular : 0 ≤ CorvajaZannier.finitePlaceOrder (↑q) z) : ∃ (c : K), 0 < CorvajaZannier.finitePlaceOrder (↑q) (z - (algebraMap K L) c)

At a rational finite place, a nonconstant regular function has a unique constant residue representative, expressed by positive order of the difference.

theorem BGS.HasseWeil.mem_valuationSubringAtPrime_of_finitePlaceOrder_nonnegative (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] (q : IsDedekindDomain.HeightOneSpectrum ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)) (z : L) (hz : z ≠ 0) (hregular : 0 ≤ CorvajaZannier.finitePlaceOrder q z) : z ∈ IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime L q

Nonnegative finite-place order is equivalent to regularity in the canonical valuation subring; this direction is the one needed below.

theorem BGS.HasseWeil.rationalBasePlace_primesOver_card_le_finrank (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : RatFuncRationalFinitePlace K) : Fintype.card ↑((↑P).asIdeal.primesOver ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)) ≤ Module.finrank (RatFunc K) L

The full lying-over fiber above a rational finite base place has at most the extension degree many primes.

noncomputable def BGS.HasseWeil.rationalFinitePlaceBaseCoordinate (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] (Q : FiniteExtensionRationalFinitePlace K L) : K

The first-coordinate value of the rational base place below a rational finite extension place.

Equations

• BGS.HasseWeil.rationalFinitePlaceBaseCoordinate K L Q = (BGS.HasseWeil.ratFuncRationalFinitePlaceEquiv K) (BGS.HasseWeil.rationalFinitePlaceToBaseFiber K L Q).fst

@[reducible, inline]

abbrev BGS.HasseWeil.RationalFinitePlaceOverPolynomialZeros (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] (R : Polynomial K) : Type u_2

Rational finite places whose base coordinate is a zero of R.

Equations

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

theorem BGS.HasseWeil.rationalFinitePlaceOverPolynomialZeros_card_le (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] [Fintype K] (R : Polynomial K) : Nat.card (RationalFinitePlaceOverPolynomialZeros K L R) ≤ Fintype.card { a : K // Polynomial.eval a R = 0 } * Module.finrank (RatFunc K) L

A base polynomial with r rational roots accounts for at most r * [L : K(X)] rational finite places.

@[reducible, inline]

abbrev BGS.HasseWeil.RationalFinitePlaceAwayFromPolynomialZeros (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] (R : Polynomial K) : Type u_2

Rational finite places whose base coordinate avoids the zero locus of R.

Equations

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

theorem BGS.HasseWeil.rationalFinitePlace_card_eq_away_add_overPolynomialZeros (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] [Finite K] (R : Polynomial K) : Nat.card (FiniteExtensionRationalFinitePlace K L) = Nat.card (RationalFinitePlaceAwayFromPolynomialZeros K L R) + Nat.card (RationalFinitePlaceOverPolynomialZeros K L R)

Rational finite places split as the places away from R = 0 and the places over R = 0.

theorem BGS.HasseWeil.finiteExtensionRationalPlaceCount_le_natCard_add_polynomialZeros_of_away_injective (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] [Fintype K] (R : Polynomial K) (A : Type u_3) [Finite A] (center : RationalFinitePlaceAwayFromPolynomialZeros K L R → A) (hcenter : Function.Injective center) : finiteExtensionRationalPlaceCount K L ≤ Nat.card A + Fintype.card { a : K // Polynomial.eval a R = 0 } * Module.finrank (RatFunc K) L + Module.finrank (RatFunc K) L

Abstract reverse counting principle. An injective center map from the rational finite places away from R = 0 into a finite type A, together with the bad-fiber and infinity estimates, bounds every rational place.

theorem BGS.HasseWeil.rationalFinitePlacePolynomial_isUnit_of_eval_baseCoordinate_ne_zero (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] (Q : FiniteExtensionRationalFinitePlace K L) (R : Polynomial K) (hR : Polynomial.eval (rationalFinitePlaceBaseCoordinate K L Q) R ≠ 0) : let V := IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime L ↑Q; IsUnit ((algebraMap (Polynomial K) ↥V) R)

A base polynomial that does not vanish at the rational base coordinate of a rational finite extension place becomes a unit in that place's valuation subring.

theorem BGS.HasseWeil.rationalFinitePlaceBaseCoordinate_residue (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] (Q : FiniteExtensionRationalFinitePlace K L) : let B := CorvajaZannier.RatFuncFiniteIntegralClosure K L; let V := IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime L ↑Q; let m := IsLocalRing.maximalIdeal ↥V; (algebraMap K m.ResidueField) (rationalFinitePlaceBaseCoordinate K L Q) = (algebraMap (↥V) m.ResidueField) ((algebraMap (Polynomial K) ↥V) Polynomial.X)

The residue of the rational-function parameter at a rational finite extension place is its recorded base coordinate.

theorem BGS.HasseWeil.planeCurveSecondCoordinate_mem_valuationSubringAtPrime_of_affineExceptional_ne_zero {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; have this_6 := Classical.decEq (RatFunc K); ∀ (Q : FiniteExtensionRationalFinitePlace K (CorvajaZannier.PlaneCurveFunctionField f)), Polynomial.eval (rationalFinitePlaceBaseCoordinate K (CorvajaZannier.PlaneCurveFunctionField f) Q) (secondCoordinateAffineExceptionalPolynomial f) ≠ 0 → CorvajaZannier.planeCurveFunction f 1 ∈ IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime (CorvajaZannier.PlaneCurveFunctionField f) ↑Q

Away from the leading-coefficient zero locus, the second plane coordinate is regular in the valuation subring of a rational finite place. The proof makes the specialized leading coefficient a unit, obtains a monic equation over the valuation ring, and uses its integral closedness.

noncomputable def BGS.HasseWeil.planeCurveGoodRationalFinitePlaceCenter {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; have this_6 := Classical.decEq (RatFunc K); RationalFinitePlaceAwayFromPolynomialZeros K (CorvajaZannier.PlaneCurveFunctionField f) (secondCoordinateAffineExceptionalPolynomial f) → CorvajaZannier.AffinePlaneCurvePoint f

The affine residue center of a rational finite normalization place away from the leading-coefficient/discriminant locus. Both plane coordinates are regular there, and the degree-one residue field identifies their residue classes with unique constants in K.

Equations

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

theorem BGS.HasseWeil.planeCurveGoodRationalFinitePlaceCenter_firstCoordinate {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; ∀ (Q : RationalFinitePlaceAwayFromPolynomialZeros K (CorvajaZannier.PlaneCurveFunctionField f) (secondCoordinateAffineExceptionalPolynomial f)), (↑(planeCurveGoodRationalFinitePlaceCenter hf hpartialSecond Q)).1 = rationalFinitePlaceBaseCoordinate K (CorvajaZannier.PlaneCurveFunctionField f) ↑Q

The first coordinate of the affine residue center is the base coordinate of the rational finite place.

theorem BGS.HasseWeil.planeCurveGoodRationalFinitePlaceCenter_secondCoordinate_residue {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; let this_6 := Classical.decEq (RatFunc K); ∀ (Q : RationalFinitePlaceAwayFromPolynomialZeros K (CorvajaZannier.PlaneCurveFunctionField f) (secondCoordinateAffineExceptionalPolynomial f)), let E := CorvajaZannier.PlaneCurveFunctionField f; let B := CorvajaZannier.RatFuncFiniteIntegralClosure K E; let V := IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime E ↑↑Q; let m := IsLocalRing.maximalIdeal ↥V; (algebraMap K m.ResidueField) (↑(planeCurveGoodRationalFinitePlaceCenter hf hpartialSecond Q)).2 = (algebraMap (↥V) m.ResidueField) ⟨CorvajaZannier.planeCurveFunction f 1, ⋯⟩

The second coordinate of the affine center represents the residue class of the second plane coordinate in the local residue field.

theorem BGS.HasseWeil.exists_planeCurveGoodRationalFinitePlace_centeredCoordinateRingHom {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; let this_6 := Classical.decEq (RatFunc K); ∀ (Q : RationalFinitePlaceAwayFromPolynomialZeros K (CorvajaZannier.PlaneCurveFunctionField f) (secondCoordinateAffineExceptionalPolynomial f)), let A := CorvajaZannier.PlaneCurveCoordinateRing f; let E := CorvajaZannier.PlaneCurveFunctionField f; have V := IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime E ↑↑Q; ∃ (φ : A →+* ↥V), (∀ (r : A), ↑(φ r) = (algebraMap A E) r) ∧ Ideal.comap φ (IsLocalRing.maximalIdeal ↥V) = (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f (planeCurveGoodRationalFinitePlaceCenter hf hpartialSecond Q)).asIdeal

A good rational finite place admits a coordinate-ring map into its valuation ring. The map is the canonical inclusion in the function field, and the inverse image of the local maximal ideal is exactly the maximal ideal of its affine residue center.

theorem BGS.HasseWeil.planeCurveGoodRationalFinitePlaceCenter_partialY_ne_zero {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; ∀ (Q : RationalFinitePlaceAwayFromPolynomialZeros K (CorvajaZannier.PlaneCurveFunctionField f) (secondCoordinateAffineExceptionalPolynomial f)), (MvPolynomial.eval ![(↑(planeCurveGoodRationalFinitePlaceCenter hf hpartialSecond Q)).1, (↑(planeCurveGoodRationalFinitePlaceCenter hf hpartialSecond Q)).2]) ((MvPolynomial.pderiv 1) f) ≠ 0

Avoiding the derivative resultant forces the affine residue center to lie in the partial-Y smooth locus.

theorem BGS.HasseWeil.planeCurveGoodRationalFinitePlace_valuationSubring_eq_dominating {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [Finite K] (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; let this_6 := Classical.decEq (RatFunc K); ∀ (Q : RationalFinitePlaceAwayFromPolynomialZeros K (CorvajaZannier.PlaneCurveFunctionField f) (secondCoordinateAffineExceptionalPolynomial f)), IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime (CorvajaZannier.PlaneCurveFunctionField f) ↑↑Q = CorvajaZannier.dominatingValuationSubring (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f (planeCurveGoodRationalFinitePlaceCenter hf hpartialSecond Q))

At a good rational finite place, the normalization valuation ring is the unique valuation ring dominating its smooth affine residue center.

theorem BGS.HasseWeil.planeCurveGoodRationalFinitePlaceCenter_injective {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [Finite K] (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; Function.Injective (planeCurveGoodRationalFinitePlaceCenter hf hpartialSecond)

The residue-center map is injective on the good rational finite places: smoothness makes the local DVR, hence the dominating valuation ring, unique.

theorem BGS.HasseWeil.planeCurveExceptionalRationalFinitePlace_card_le {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [Finite K] {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; Nat.card (RationalFinitePlaceOverPolynomialZeros K (CorvajaZannier.PlaneCurveFunctionField f) (secondCoordinateAffineExceptionalPolynomial f)) ≤ (firstDegree + (2 * secondDegree - 1) * firstDegree) * secondDegree

Plane-curve specialization of the bad-fiber estimate. Rational finite places over a base fiber where either the second-coordinate leading coefficient vanishes or the second-coordinate derivative has a common root are controlled only by the bidegree.

theorem BGS.HasseWeil.finiteExtensionRationalPlaceCount_le_affine_add_exceptional_of_away_injective {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; ∀ (center : RationalFinitePlaceAwayFromPolynomialZeros K (CorvajaZannier.PlaneCurveFunctionField f) (secondCoordinateAffineExceptionalPolynomial f) → CorvajaZannier.AffinePlaneCurvePoint f), Function.Injective center → finiteExtensionRationalPlaceCount K (CorvajaZannier.PlaneCurveFunctionField f) ≤ Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f) + (firstDegree + (2 * secondDegree - 1) * firstDegree) * secondDegree + secondDegree

Conditional reverse affine-normalization comparison. Once the geometric center construction is supplied as an injection from rational finite places away from the leading-coefficient/discriminant locus, the total rational place count is bounded by affine points, the exceptional finite fibers, and the places at infinity.

theorem BGS.HasseWeil.finiteExtensionRationalPlaceCount_le_affine_add_exceptional {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; finiteExtensionRationalPlaceCount K (CorvajaZannier.PlaneCurveFunctionField f) ≤ Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f) + (firstDegree + (2 * secondDegree - 1) * firstDegree) * secondDegree + secondDegree

Unconditional reverse affine-normalization comparison. Good rational finite places inject into affine rational points, exceptional finite fibers are controlled by the leading-coefficient/resultant polynomial, and infinity contributes at most the second-coordinate degree.