Finite places centered at affine rational points

For an irreducible plane curve with both coordinates separating, this file chooses an exhaustive finite place centered at each affine rational point. Both coordinate differences have positive order at the selected place, and distinct affine points give distinct places.

The construction records the affine center through equality of valuation subrings. It deliberately makes no residue-degree-one claim: above a singular rational point, a chosen normalization branch need not be rational.

theorem BGS.HasseWeil.firstCoordinate_sub_mem_affinePlaneCurvePointMaximalIdeal {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (z : CorvajaZannier.AffinePlaneCurvePoint f) : CorvajaZannier.planeCurveCoordinate f 0 - (algebraMap K (CorvajaZannier.PlaneCurveCoordinateRing f)) (↑z).1 ∈ (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f z).asIdeal

The first coordinate minus its value at an affine point belongs to the point's maximal ideal.

theorem BGS.HasseWeil.secondCoordinate_sub_mem_affinePlaneCurvePointMaximalIdeal {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (z : CorvajaZannier.AffinePlaneCurvePoint f) : CorvajaZannier.planeCurveCoordinate f 1 - (algebraMap K (CorvajaZannier.PlaneCurveCoordinateRing f)) (↑z).2 ∈ (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f z).asIdeal

The second coordinate minus its value at an affine point belongs to the point's maximal ideal.

theorem BGS.HasseWeil.firstCoordinate_sub_affinePoint_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (z : CorvajaZannier.AffinePlaneCurvePoint f) : CorvajaZannier.planeCurveFunction f 0 - (algebraMap K (CorvajaZannier.PlaneCurveFunctionField f)) (↑z).1 ≠ 0

A separating first coordinate cannot equal the constant first coordinate of an affine point in the function field.

theorem BGS.HasseWeil.secondCoordinate_sub_affinePoint_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (z : CorvajaZannier.AffinePlaneCurvePoint f) : CorvajaZannier.planeCurveFunction f 1 - (algebraMap K (CorvajaZannier.PlaneCurveFunctionField f)) (↑z).2 ≠ 0

A separating second coordinate cannot equal the constant second coordinate of an affine point in the function field.

theorem BGS.HasseWeil.exists_affinePoint_exhaustiveFinitePlace_orders_positive {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (z : CorvajaZannier.AffinePlaneCurvePoint f) : 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 := ⋯; have this_7 := ⋯; ∃ (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial K) (CorvajaZannier.PlaneCurveFunctionField f))), IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime (CorvajaZannier.PlaneCurveFunctionField f) q = CorvajaZannier.dominatingValuationSubring (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f z) ∧ 0 < CorvajaZannier.finitePlaceOrder q (CorvajaZannier.planeCurveFunction f 0 - (algebraMap K (CorvajaZannier.PlaneCurveFunctionField f)) (↑z).1) ∧ 0 < CorvajaZannier.finitePlaceOrder q (CorvajaZannier.planeCurveFunction f 1 - (algebraMap K (CorvajaZannier.PlaneCurveFunctionField f)) (↑z).2)

Every affine rational point has an exhaustive finite place centered at that point where both coordinate differences have positive order.

noncomputable def BGS.HasseWeil.affinePointExhaustiveFinitePlace {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (z : CorvajaZannier.AffinePlaneCurvePoint f) : have hx := ⋯; CorvajaZannier.FiniteExtensionFinitePlace K (CorvajaZannier.PlaneCurveFunctionField f)

The exhaustive finite place selected above an affine rational point.

Equations

• BGS.HasseWeil.affinePointExhaustiveFinitePlace hf hpartialFirst hpartialSecond z = Classical.choose ⋯

theorem BGS.HasseWeil.affinePointExhaustiveFinitePlace_spec {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (z : CorvajaZannier.AffinePlaneCurvePoint f) : have hx := ⋯; IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime (CorvajaZannier.PlaneCurveFunctionField f) (affinePointExhaustiveFinitePlace hf hpartialFirst hpartialSecond z) = CorvajaZannier.dominatingValuationSubring (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f z) ∧ 0 < CorvajaZannier.finitePlaceOrder (affinePointExhaustiveFinitePlace hf hpartialFirst hpartialSecond z) (CorvajaZannier.planeCurveFunction f 0 - (algebraMap K (CorvajaZannier.PlaneCurveFunctionField f)) (↑z).1) ∧ 0 < CorvajaZannier.finitePlaceOrder (affinePointExhaustiveFinitePlace hf hpartialFirst hpartialSecond z) (CorvajaZannier.planeCurveFunction f 1 - (algebraMap K (CorvajaZannier.PlaneCurveFunctionField f)) (↑z).2)

The selected finite place has the prescribed affine center, and both coordinate differences have positive order there.

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

Distinct affine rational points have distinct selected exhaustive finite places. The proof uses equality of affine centers, not residue degrees.

theorem BGS.HasseWeil.finitePlaceOrder_affinePointExhaustiveFinitePlace_pos_of_mem {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (z : CorvajaZannier.AffinePlaneCurvePoint f) (r : CorvajaZannier.PlaneCurveCoordinateRing f) (hr : r ∈ (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f z).asIdeal) (hr0 : (algebraMap (CorvajaZannier.PlaneCurveCoordinateRing f) (CorvajaZannier.PlaneCurveFunctionField f)) r ≠ 0) : have hx := ⋯; 0 < CorvajaZannier.finitePlaceOrder (affinePointExhaustiveFinitePlace hf hpartialFirst hpartialSecond z) ((algebraMap (CorvajaZannier.PlaneCurveCoordinateRing f) (CorvajaZannier.PlaneCurveFunctionField f)) r)

Any nonzero regular function vanishing at an affine point has positive order at that point's selected finite place.

theorem BGS.HasseWeil.affinePointFamily_card_le_finiteExtensionGcdWeightedDegree {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [DecidableEq K] {ι : Type u_2} [Fintype ι] (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (point : ι → CorvajaZannier.AffinePlaneCurvePoint f) (hpoint : Function.Injective point) (r s : CorvajaZannier.PlaneCurveCoordinateRing f) (hr : ∀ (i : ι), r ∈ (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f (point i)).asIdeal) (hs : ∀ (i : ι), s ∈ (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f (point i)).asIdeal) (hr0 : (algebraMap (CorvajaZannier.PlaneCurveCoordinateRing f) (CorvajaZannier.PlaneCurveFunctionField f)) r ≠ 0) (hs0 : (algebraMap (CorvajaZannier.PlaneCurveCoordinateRing f) (CorvajaZannier.PlaneCurveFunctionField f)) s ≠ 0) : have hx := ⋯; Fintype.card ι ≤ CorvajaZannier.finiteExtensionGcdWeightedDegree K (CorvajaZannier.PlaneCurveFunctionField f) ((algebraMap (CorvajaZannier.PlaneCurveCoordinateRing f) (CorvajaZannier.PlaneCurveFunctionField f)) r) ((algebraMap (CorvajaZannier.PlaneCurveCoordinateRing f) (CorvajaZannier.PlaneCurveFunctionField f)) s)

A finite family of distinct affine rational points at which two fixed nonzero regular functions vanish is bounded by their degree-weighted positive gcd divisor. Positive place degree suffices; no selected place is asserted to have degree one.