Nonsingularity of projective points on an elliptic curve

Over a field, every nonzero point representative [X : Y : Z] satisfying the projective Weierstrass equation of an elliptic curve is nonsingular. This is the projective counterpart of Mathlib's WeierstrassCurve.Affine.equation_iff_nonsingular. The hypothesis that the representative is nonzero is necessary: (0, 0, 0) satisfies the homogeneous equation but all three partial derivatives vanish there.

Main results

• WeierstrassCurve.Projective.equation_iff_nonsingular_of_Δ_ne_zero_of_ne_zero: over a field, if the discriminant is nonzero, a nonzero point representative satisfies the equation if and only if it is nonsingular.
• WeierstrassCurve.Projective.equation_iff_nonsingular_of_ne_zero: on an elliptic curve over a field, a nonzero point representative satisfies the equation if and only if it is nonsingular.

theorem WeierstrassCurve.Projective.equation_iff_nonsingular_of_Δ_ne_zero_of_ne_zero {F : Type u_1} [Field F] {W : Projective F} (hΔ : Δ W ≠ 0) {P : Fin 3 → F} (hP : P ≠ 0) : W.Equation P ↔ W.Nonsingular P

Over a field, if the discriminant is nonzero, then a nonzero point representative satisfies the projective Weierstrass equation if and only if it is nonsingular. If Z ≠ 0, this is the affine statement; if Z = 0, the equation forces X = 0, and then Y ≠ 0 makes W_Z = Y² nonzero.

theorem WeierstrassCurve.Projective.equation_iff_nonsingular_of_ne_zero {F : Type u_1} [Field F] {W : Projective F} [WeierstrassCurve.IsElliptic W] {P : Fin 3 → F} (hP : P ≠ 0) : W.Equation P ↔ W.Nonsingular P

On an elliptic curve over a field, a nonzero point representative satisfies the projective Weierstrass equation if and only if it is nonsingular.