Point counts at a singular Weierstrass model

The projective equation points of a Weierstrass model split into its nonsingular affine points, its singular affine points, and the point at infinity. Mathlib's WeierstrassCurve.Affine.Point contains the first and third parts. Consequently, pointCount is the cardinality of that point type plus the number of rational singular points whenever the affine equation has finitely many rational solutions. The base field itself need not be finite for these comparisons.

Over a field a Weierstrass model has at most one singular point. Thus a rational singular point contributes exactly one to pointCount; the theorem pointCount_eq_card_point_add_one_iff characterises this case.

Over a finite field of q elements the singular point is rational and the count is explicit. Move the singular point to the origin, where the equation reads y² + a₁ x y = x³ + a₂ x². Away from the origin a solution has x ≠ 0, and its slope t = y / x determines it: x = t² + a₁ t − a₂, and t is not a root of the tangent quadratic T² + a₁ T − a₂. So the model has q + 2 − r points, where r counts the rational tangent slopes, and its Frobenius trace q + 1 − pointCount is r − 1. The node polynomial is c₄ times the tangent quadratic, and the discriminant of that quadratic squares to c₄. The three shapes of singularity therefore give the three classical local invariants: 1 at a split node, −1 at a nonsplit node and 0 at a cusp.

Main results

• WeierstrassCurve.pointCount_eq_card_point_add_card_singular: the projective equation count is the nonsingular point count plus the number of singular affine points.
• WeierstrassCurve.pointCount_eq_card_point_add_one_of_isSingular: a given rational singular point contributes exactly one.
• WeierstrassCurve.pointCount_eq_card_point_add_one_iff: adding one is equivalent to the existence of a rational singular point.
• WeierstrassCurve.frobeniusTrace_eq_one_of_splits, WeierstrassCurve.frobeniusTrace_eq_neg_one_of_not_splits and WeierstrassCurve.frobeniusTrace_eq_zero_of_c₄_eq_zero: over a finite field, the trace of a singular model is 1 at a split node, −1 at a nonsplit node and 0 at a cusp.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.1, III.2.5, V.1.

theorem WeierstrassCurve.pointCount_eq_card_point_add_card_singular {F : Type u_1} [Field F] (W : WeierstrassCurve F) [Finite { p : F × F // W.toAffine.Equation p.1 p.2 }] : W.pointCount = Nat.card W.toAffine.Point + Nat.card { p : F × F // W.toAffine.IsSingular p.1 p.2 }

The projective equation count is the nonsingular point count plus the number of rational singular affine points. The point at infinity occurs in both pointCount and Mathlib's point type, while the affine equation points split into their nonsingular and singular parts. Only the affine solution type needs to be finite.

theorem WeierstrassCurve.pointCount_eq_card_point_add_one_of_isSingular {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x y : F} (h : W.toAffine.IsSingular x y) : W.pointCount = Nat.card W.toAffine.Point + 1

A rational singular point contributes exactly one to the projective equation count. There cannot be another one because a Weierstrass model over a field has at most one singular point.

theorem WeierstrassCurve.pointCount_eq_card_point_add_one_iff {F : Type u_1} [Field F] (W : WeierstrassCurve F) [Finite { p : F × F // W.toAffine.Equation p.1 p.2 }] : W.pointCount = Nat.card W.toAffine.Point + 1 ↔ ∃ (x : F) (y : F), W.toAffine.IsSingular x y

The projective equation count exceeds the nonsingular point count by one exactly when the model has a rational singular affine point.

theorem WeierstrassCurve.frobeniusTrace_eq_zero_of_c₄_eq_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) [Finite F] (hΔ : W.Δ = 0) (hc₄ : W.c₄ = 0) : W.frobeniusTrace = 0

The Frobenius trace at a cusp is 0. A singular model over a finite field with c₄ = 0 has one tangent slope at its singular point, and q nonsingular points, the point at infinity included.

theorem WeierstrassCurve.frobeniusTrace_eq_one_of_splits {F : Type u_1} [Field F] (W : WeierstrassCurve F) [Finite F] (hΔ : W.Δ = 0) (hc₄ : W.c₄ ≠ 0) (hs : W.nodePolynomial.Splits) : W.frobeniusTrace = 1

The Frobenius trace at a split node is 1. A singular model over a finite field with c₄ ≠ 0 whose node polynomial splits has two rational tangent slopes at its node, and q - 1 nonsingular points, the point at infinity included.

theorem WeierstrassCurve.frobeniusTrace_eq_neg_one_of_not_splits {F : Type u_1} [Field F] (W : WeierstrassCurve F) [Finite F] (hΔ : W.Δ = 0) (hs : ¬W.nodePolynomial.Splits) : W.frobeniusTrace = -1

The Frobenius trace at a nonsplit node is -1. A singular model over a finite field whose node polynomial does not split has no rational tangent slope at its node, and q + 1 nonsingular points, the point at infinity included.