Supersingular and ordinary Weierstrass curves

An elliptic curve E over a field K of characteristic p > 0 is supersingular when it has no nonzero geometric point of order p, that is E[p](AlgebraicClosure K) = O, and ordinary otherwise (Silverman V.3.1). The definition here is this geometric one, read over Mathlib's AlgebraicClosure K, and it makes sense over an arbitrary field of characteristic p, where there is in general no trace of Frobenius.

The geometric points must be taken over an algebraic closure, not a separable one. Over an imperfect field an ordinary curve can have all of its nonzero p-torsion purely inseparable over K: over 𝔽₂(t) the curve y² + xy = x³ + t has j = 1 / t ≠ 0, so it is ordinary, but its only nonzero 2-torsion point is (0, √t), which does not lie over the separable closure. A separable-closure definition would call this curve supersingular, and would make supersingularity change under the purely inseparable extension 𝔽₂(√t) / 𝔽₂(t).

With the algebraic closure, the choice of closure does not matter: an extension of an algebraically closed field adds no torsion (WeierstrassCurve.torsionBy_baseChange_eq_bot_iff_of_isAlgClosed), so the p-torsion may be read over any algebraically closed extension of K. It follows that supersingularity is invariant under every field extension L / K, algebraic or not.

In characteristic 2 and 3 supersingularity is decided by the j-invariant. There the polynomial whose roots are the abscissae of the nonzero p-torsion is a₁²x² + a₃², respectively (b₂x³ + b₈)², and on an elliptic curve it is a nonzero constant exactly when j = 0.

Main definitions

• WeierstrassCurve.IsSupersingular: W has no nonzero p-torsion point over AlgebraicClosure K.
• WeierstrassCurve.IsOrdinary: W is not supersingular.

Main results

• WeierstrassCurve.isSupersingular_iff_of_isAlgClosed: the p-torsion may be read over any algebraically closed extension of K.
• WeierstrassCurve.isSupersingular_baseChange_iff: supersingularity is invariant under an arbitrary field extension.
• WeierstrassCurve.isSupersingular_variableChange_iff: it is invariant under changes of variables.
• WeierstrassCurve.isSupersingular_iff_forall_pow: a supersingular curve has no nonzero p ^ r-torsion over AlgebraicClosure K for any r.
• WeierstrassCurve.isSupersingular_iff_j_eq_zero_of_char_two and WeierstrassCurve.isSupersingular_iff_j_eq_zero_of_char_three: in characteristic 2 and 3, an elliptic curve is supersingular exactly when j = 0.
• WeierstrassCurve.isOrdinary_iff_j_ne_zero_of_char_two and WeierstrassCurve.isOrdinary_iff_j_ne_zero_of_char_three: in characteristic 2 and 3, an elliptic curve is ordinary exactly when j ≠ 0.

References

• J. Silverman, The Arithmetic of Elliptic Curves, V.3.1, V.4.1 and Appendix A.

def WeierstrassCurve.IsSupersingular {K : Type u_1} [Field K] (p : ℕ) (W : WeierstrassCurve K) : Prop

A supersingular Weierstrass curve at p: the curve has no nonzero point of order dividing p over the algebraic closure of K. For an elliptic curve over a field of characteristic p > 0 this is supersingularity in the sense of Silverman V.3.1.

Equations

• WeierstrassCurve.IsSupersingular p W = (AddSubgroup.torsionBy (W.baseChange (AlgebraicClosure K)).toAffine.Point ↑p = ⊥)

def WeierstrassCurve.IsOrdinary {K : Type u_1} [Field K] (p : ℕ) (W : WeierstrassCurve K) : Prop

An ordinary Weierstrass curve at p: the curve is not supersingular at p, so it has a nonzero p-torsion point over the algebraic closure of K.

Equations

• WeierstrassCurve.IsOrdinary p W = ¬WeierstrassCurve.IsSupersingular p W

@[simp]

theorem WeierstrassCurve.not_isSupersingular {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} : ¬IsSupersingular p W ↔ IsOrdinary p W

A curve that is not supersingular is ordinary.

@[simp]

theorem WeierstrassCurve.not_isOrdinary {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} : ¬IsOrdinary p W ↔ IsSupersingular p W

A curve that is not ordinary is supersingular.

theorem WeierstrassCurve.isSupersingular_iff_forall {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} : IsSupersingular p W ↔ ∀ (P : (W.baseChange (AlgebraicClosure K)).toAffine.Point), p • P = 0 → P = 0

Supersingularity unfolded: every p-torsion point over AlgebraicClosure K is zero.

theorem WeierstrassCurve.isOrdinary_iff_exists {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} : IsOrdinary p W ↔ ∃ (P : (W.baseChange (AlgebraicClosure K)).toAffine.Point), p • P = 0 ∧ P ≠ 0

An ordinary curve has a nonzero p-torsion point over AlgebraicClosure K.

theorem WeierstrassCurve.isSupersingular_iff_forall_pow {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} : IsSupersingular p W ↔ ∀ (r : ℕ), AddSubgroup.torsionBy (W.baseChange (AlgebraicClosure K)).toAffine.Point (↑p ^ r) = ⊥

A supersingular curve has no geometric p-power torsion: if E[p](AlgebraicClosure K) = O then E[p ^ r](AlgebraicClosure K) = O for every r.

theorem WeierstrassCurve.isSupersingular_iff_of_isAlgClosed {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} [W.IsElliptic] (hp : p ≠ 0) (Ω : Type u_2) [Field Ω] [IsAlgClosed Ω] [Algebra K Ω] [DecidableEq Ω] : IsSupersingular p W ↔ AddSubgroup.torsionBy (W.baseChange Ω).toAffine.Point ↑p = ⊥

Supersingularity may be read over any algebraically closed extension Ω of K: the p-torsion of W over Ω is trivial exactly when it is over AlgebraicClosure K, since AlgebraicClosure K embeds into Ω and an extension of an algebraically closed field adds no torsion.

theorem WeierstrassCurve.isSupersingular_baseChange_iff {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} [W.IsElliptic] (hp : p ≠ 0) (L : Type u_2) [Field L] [Algebra K L] : IsSupersingular p (W.baseChange L) ↔ IsSupersingular p W

Supersingularity is invariant under field extension: for an arbitrary extension L / K, not necessarily algebraic, W is supersingular exactly when its base change to L is.

theorem WeierstrassCurve.isOrdinary_baseChange_iff {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} [W.IsElliptic] (hp : p ≠ 0) (L : Type u_2) [Field L] [Algebra K L] : IsOrdinary p (W.baseChange L) ↔ IsOrdinary p W

Ordinarity is invariant under field extension.

@[simp]

theorem WeierstrassCurve.isSupersingular_variableChange_iff {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} (C : VariableChange K) : IsSupersingular p (C • W) ↔ IsSupersingular p W

Supersingularity is invariant under a change of variables: isomorphic Weierstrass curves have isomorphic point groups over AlgebraicClosure K.

@[simp]

theorem WeierstrassCurve.isOrdinary_variableChange_iff {K : Type u_1} [Field K] {p : ℕ} {W : WeierstrassCurve K} (C : VariableChange K) : IsOrdinary p (C • W) ↔ IsOrdinary p W

Ordinarity is invariant under a change of variables.

Characteristic two and three

theorem WeierstrassCurve.isSupersingular_iff_j_eq_zero_of_char_two {K : Type u_1} [Field K] {W : WeierstrassCurve K} [W.IsElliptic] [CharP K 2] : IsSupersingular 2 W ↔ W.j = 0

In characteristic 2 an elliptic curve is supersingular exactly when j = 0, equivalently a₁ = 0 (WeierstrassCurve.j_eq_zero_iff_of_char_two).

theorem WeierstrassCurve.isSupersingular_iff_j_eq_zero_of_char_three {K : Type u_1} [Field K] {W : WeierstrassCurve K} [W.IsElliptic] [CharP K 3] : IsSupersingular 3 W ↔ W.j = 0

In characteristic 3 an elliptic curve is supersingular exactly when j = 0, equivalently b₂ = 0 (WeierstrassCurve.j_eq_zero_iff_of_char_three).

theorem WeierstrassCurve.isOrdinary_iff_j_ne_zero_of_char_two {K : Type u_1} [Field K] {W : WeierstrassCurve K} [W.IsElliptic] [CharP K 2] : IsOrdinary 2 W ↔ W.j ≠ 0

In characteristic 2 an elliptic curve is ordinary exactly when j ≠ 0.

theorem WeierstrassCurve.isOrdinary_iff_j_ne_zero_of_char_three {K : Type u_1} [Field K] {W : WeierstrassCurve K} [W.IsElliptic] [CharP K 3] : IsOrdinary 3 W ↔ W.j ≠ 0

In characteristic 3 an elliptic curve is ordinary exactly when j ≠ 0.