Affine plane points and rational normalization places

For an irreducible plane curve with both coordinates separating, every affine point that is regular in the second-coordinate direction determines a degree-one finite place of the function field. Distinct regular affine points give distinct places. Consequently the regular affine locus injects into the rational finite places, and adding the explicit critical locus compares all affine rational points with the full rational-place count.

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

Send a second-coordinate regular affine point to its selected degree-one finite normalization place.

Equations

• BGS.HasseWeil.affineSecondCoordinateRegularPointToRationalFinitePlace hf hpartialFirst hpartialSecond z = ⟨BGS.HasseWeil.affinePointExhaustiveFinitePlace hf hpartialFirst hpartialSecond ↑z, ⋯⟩

theorem BGS.HasseWeil.affineSecondCoordinateRegularPointToRationalFinitePlace_injective {K : Type u_1} [Field K] [Fintype K] [DecidableEq 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 (affineSecondCoordinateRegularPointToRationalFinitePlace hf hpartialFirst hpartialSecond)

Distinct second-coordinate regular affine points determine distinct degree-one finite normalization places.

theorem BGS.HasseWeil.affineSecondCoordinateRegularPoint_card_le_rationalFinitePlace {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; Fintype.card (AffineSecondCoordinateRegularPoint f) ≤ Nat.card (FiniteExtensionRationalFinitePlace K (CorvajaZannier.PlaneCurveFunctionField f))

The regular affine locus has cardinality at most the number of degree-one finite places.

theorem BGS.HasseWeil.affineSecondCoordinateRegularPoint_card_le_rationalPlaceCount {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; Fintype.card (AffineSecondCoordinateRegularPoint f) ≤ finiteExtensionRationalPlaceCount K (CorvajaZannier.PlaneCurveFunctionField f)

The regular affine locus has cardinality at most the total rational-place count, which also includes places above infinity.

theorem BGS.HasseWeil.affinePlaneCurvePoint_card_le_rationalPlaceCount_add_critical {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f) ≤ finiteExtensionRationalPlaceCount K (CorvajaZannier.PlaneCurveFunctionField f) + (affineSecondCoordinateCriticalPoints K f).card

The first affine-normalization comparison: all affine rational points are bounded by the rational places of the normalization plus the explicit second-coordinate critical locus.