Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.PlaneRegularPointCount

Regular affine points in the second-coordinate direction #

The Stepanov argument is applied only at affine points where the second partial derivative is nonzero. At those points the affine local ring agrees with the normalization local ring, so the selected normalization place has residue degree one. The complementary critical points are kept explicit and are bounded by affineSecondCoordinateCriticalPoints_card_le.

This file contains only the finite-set bookkeeping. The local normalization statement and the Stepanov zero count are proved in separate modules.

source
@[reducible, inline]
abbrev BGS.HasseWeil.AffineSecondCoordinateRegularPoint {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) :
Type u_1

Affine points where differentiation in the second coordinate is regular.

Equations
Instances For
    source
    def BGS.HasseWeil.affineSecondCoordinateNonregularEquivCritical {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) :
    { z : CorvajaZannier.AffinePlaneCurvePoint f // ¬(MvPolynomial.eval ![(↑z).1, (↑z).2]) ((MvPolynomial.pderiv 1) f) ≠ 0 } ≃ ↥(affineSecondCoordinateCriticalPoints K f)

    The complement of the regular-point subtype is the finite critical locus.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.HasseWeil.affinePlaneCurvePoint_card_eq_regular_add_critical {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) :
      Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f) = Fintype.card (AffineSecondCoordinateRegularPoint f) + (affineSecondCoordinateCriticalPoints K f).card

      Every affine point is either regular in the second-coordinate direction or belongs to the explicitly defined critical locus.

      source
      theorem BGS.HasseWeil.regularPoint_card_eq_punctured_add_one {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (z₀ : AffineSecondCoordinateRegularPoint f) :
      Fintype.card (AffineSecondCoordinateRegularPoint f) = Fintype.card { z : AffineSecondCoordinateRegularPoint f // z ≠ z₀ } + 1

      Removing one chosen regular point lowers the regular-point cardinality by exactly one. This is the form needed when that point supplies the unique allowed pole of the Stepanov auxiliary.