Supersingular elliptic curves

DefinitionSupersingular elliptic curves#✓fully proved

Let \(p\) be a prime and let \(E\) be an elliptic curve over an algebraic closure \(\overline{\mathbb{F}}_p\) of \(\mathbb{Z}/p\mathbb{Z}\). Then \(E\) is called supersingular when every point \(P \in E(\overline{\mathbb{F}}_p)\) with \(pP = 0\) is \(P = 0\).

def IsSupersingular {p : ℕ} [Fact p.Prime]
    (W : WeierstrassCurve.Affine (AlgebraicClosure (ZMod p))) [W.IsElliptic] : Prop :=
  ∀ P : W.Point, p • P = 0 → P = 0

Sources

• arXiv:2308.11539v1, main.tex, lines 164–170, which gives the equivalent condition that for every positive integer \(r\), every point \(P\) with \(p^r P = 0\) is \(P = 0\); this definition is its case \(r = 1\).

Used by 2

Used bySupersingularity from trivial prime-power torsion · Supersingular curves have trivial prime-power torsion

TheoremSupersingularity from trivial prime-power torsion#✓fully proved

Let \(p\) be a prime and let \(E\) be an elliptic curve over an algebraic closure \(\overline{\mathbb{F}}_p\) of \(\mathbb{Z}/p\mathbb{Z}\). If for every integer \(r \ge 1\) the only point \(P \in E(\overline{\mathbb{F}}_p)\) with \(p^r P = 0\) is \(P = 0\), then \(E\) is supersingular.

theorem IsSupersingular.of_pow_torsion {p : ℕ} [Fact p.Prime]
    (W : WeierstrassCurve.Affine (AlgebraicClosure (ZMod p))) [W.IsElliptic]
    (h : ∀ r : ℕ, 0 < r → ∀ P : W.Point, (p ^ r) • P = 0 → P = 0) :
    W.IsSupersingular

Uses 1

Statement usesSupersingular elliptic curves

TheoremSupersingular curves have trivial prime-power torsion#✓fully proved

Let \(p\) be a prime and let \(E\) be a supersingular elliptic curve over an algebraic closure \(\overline{\mathbb{F}}_p\) of \(\mathbb{Z}/p\mathbb{Z}\). Then for every integer \(r \ge 1\), every point \(P \in E(\overline{\mathbb{F}}_p)\) with \(p^r P = 0\) is \(P = 0\).

theorem IsSupersingular.pow_torsion {p : ℕ} [Fact p.Prime]
    (W : WeierstrassCurve.Affine (AlgebraicClosure (ZMod p))) [W.IsElliptic]
    (h : W.IsSupersingular) {r : ℕ} (hr : 0 < r)
    {P : W.Point} (hP : (p ^ r) • P = 0) : P = 0

Uses 1

Statement usesSupersingular elliptic curves

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.