Documentation

Atlas.EllipticCurves.code.OrdinarySupersingular

noncomputable def OrdinarySupersingular.separableDegree {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) :

The separable degree of an isogeny φ : E₁ → E₂, i.e., the degree of the separable part of the induced extension of function fields.

Instances For

    The separable degree of an isogeny is strictly positive.

    theorem OrdinarySupersingular.separableDegree_comp {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ E₃ : WeierstrassCurve.Affine F} (ψ : Isogeny E₂ E₃) (φ : Isogeny E₁ E₂) :

    Separable degree is multiplicative under composition of isogenies.

    noncomputable def OrdinarySupersingular.mulByPIsogeny {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (p : ) [Fact (Nat.Prime p)] [CharP F p] :

    The multiplication-by-p map [p] : E → E viewed as an isogeny, where p is the characteristic of the base field.

    Instances For

      The multiplication-by-p isogeny acts on points by the usual -scalar multiplication by p.

      For any isogeny φ : E₁ → E₂, pre- and post-composition with the multiplication-by-p maps yield isogenies with the same separable degree.

      The p-torsion subgroup of E: the set of points P killed by multiplication by p.

      Instances For

        An elliptic curve E over a field of characteristic p is supersingular if its p-torsion subgroup is trivial.

        Instances For

          An elliptic curve E over a field of characteristic p is ordinary if it admits a nonzero p-torsion point.

          Instances For

            E is ordinary iff it is not supersingular.

            Supersingularity is equivalent to the multiplication-by-p isogeny having separable degree 1 (i.e., being purely inseparable).

            Every elliptic curve over a field of characteristic p is either ordinary or supersingular.

            Isogenous elliptic curves have the same separable degree for their multiplication-by-p isogenies; in particular, this is an isogeny invariant.

            Supersingularity is an isogeny invariant: if E₁ and E₂ are isogenous, then E₁ is supersingular iff E₂ is.

            Scalar multiplication by an integer m (acting on E.Point via m • id) gives a well-defined algebraic endomorphism of E.

            The endomorphism of E given by multiplication by the integer m, packaged as an element of the endomorphism ring of E.

            Instances For

              The Frobenius endomorphism of E over a finite field F of characteristic p, as an element of the endomorphism ring.

              Instances For

                The dual (Verschiebung) of the Frobenius endomorphism, as an element of the endomorphism ring.

                Instances For

                  The Frobenius endomorphism is inseparable.

                  The defining identity π + π̂ = [t] in the endomorphism ring: Frobenius plus its dual equals multiplication by the trace of Frobenius.

                  Multiplication-by-m is inseparable iff p ∣ m.

                  Supersingularity of E/F_q is equivalent to inseparability of the dual Frobenius.

                  Supersingularity of E/F_q is equivalent to p dividing the trace of Frobenius. The proof uses Lemma 7.1: if α is an inseparable isogeny, then α + β is inseparable iff β is.

                  theorem OrdinarySupersingular.jInvariant_pow_frobenius {F : Type u} [Field F] (A B : F) (p : ) [Fact (Nat.Prime p)] [CharP F p] :
                  jInvariant (A ^ p ^ 2) (B ^ p ^ 2) = jInvariant A B ^ p ^ 2

                  Frobenius compatibility of the j-invariant: applying the p^2-power Frobenius to the coefficients A, B and to the resulting j-invariant agree.

                  theorem OrdinarySupersingular.supersingular_frobeniusTwist_iso {F : Type u} [Field F] [DecidableEq F] (A B : F) (p : ) [Fact (Nat.Prime p)] [CharP F p] (hss : IsSupersingular { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := A, a₆ := B } p) :
                  ∃ (μ : F), μ 0 A ^ p ^ 2 = μ ^ 4 * A B ^ p ^ 2 = μ ^ 6 * B

                  If E : y² = x³ + Ax + B is supersingular, then E is isomorphic to its -Frobenius twist: there exists μ ≠ 0 with A^(p²) = μ⁴ A and B^(p²) = μ⁶ B.

                  theorem OrdinarySupersingular.supersingular_jInvariant_eq_frobeniusTwist {F : Type u} [Field F] [DecidableEq F] (A B : F) (p : ) [Fact (Nat.Prime p)] [CharP F p] (hss : IsSupersingular { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := A, a₆ := B } p) :
                  jInvariant A B = jInvariant (A ^ p ^ 2) (B ^ p ^ 2)

                  A supersingular curve has the same j-invariant as its -Frobenius twist.

                  theorem OrdinarySupersingular.supersingular_jInvariant_in_Fp2 {F : Type u} [Field F] [DecidableEq F] (A B : F) (p : ) [Fact (Nat.Prime p)] [CharP F p] (hss : IsSupersingular { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := A, a₆ := B } p) :
                  jInvariant A B ^ p ^ 2 = jInvariant A B

                  The j-invariant of a supersingular elliptic curve lies in F_{p²}: it is fixed by the -power Frobenius.

                  The geometric endomorphism algebra of E: End(E_{\bar F}) ⊗_ℤ ℚ, the endomorphism algebra of E after base-change to the algebraic closure.

                  Instances For
                    @[implicit_reducible]

                    Ring structure on the geometric endomorphism algebra.

                    @[implicit_reducible]

                    -algebra structure on the geometric endomorphism algebra.

                    The geometric endomorphism algebra of E is finite-dimensional over .

                    @[implicit_reducible]

                    Positive-definite involution algebra structure (Rosati involution) on the geometric endomorphism algebra of E.

                    The geometric endomorphism algebra of any elliptic curve falls into the three-way Albert classification (rational / imaginary quadratic / quaternion).

                    The predicate that the geometric endomorphism algebra of E is a quaternion algebra: it has -dimension 4 with two anticommuting elements squaring to negative rationals.

                    Instances For

                      For a supersingular elliptic curve, the geometric endomorphism algebra has -dimension strictly greater than 1, i.e., it is not just .

                      For a supersingular elliptic curve, the geometric endomorphism algebra is not an imaginary quadratic field, i.e., its -dimension is not 2.

                      The geometric endomorphism algebra of a supersingular elliptic curve is a quaternion algebra (over ).

                      If the geometric endomorphism algebra of E is a quaternion algebra, there exist two nonzero anticommuting endomorphisms α, β in the endomorphism ring of E.

                      theorem OrdinarySupersingular.ordinary_torsion_anticommutation_contradiction {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (p : ) [Fact (Nat.Prime p)] [CharP F p] (hord : IsOrdinary E p) (α β : EllipticCurve.EndomorphismRing E) ( : α 0) ( : β 0) (hanti : α * β + β * α = 0) :

                      For an ordinary elliptic curve, two nonzero anticommuting endomorphisms cannot exist: the existence of a nontrivial p-torsion point contradicts the anticommutation relation.

                      The geometric endomorphism algebra of an ordinary elliptic curve is not a quaternion algebra.

                      If the geometric endomorphism algebra of E is a quaternion algebra, then E is supersingular.

                      The predicate that the geometric endomorphism algebra of E is an imaginary quadratic field: it has -dimension 2 with a non-rational element squaring to a negative rational.

                      Instances For

                        The geometric endomorphism algebra of an ordinary elliptic curve over a finite field is an imaginary quadratic field.

                        The supersingular/ordinary dichotomy over a finite field: every elliptic curve E/F_q is either supersingular (in which case p divides the trace of Frobenius and the geometric endomorphism algebra is a quaternion algebra) or ordinary (in which case p does not divide the trace and the algebra is an imaginary quadratic field).

                        If the conductor-f₁ order is contained in the conductor-f₂ order, then f₂ ∣ f₁. This is the standard correspondence between containment of orders and divisibility of conductors.

                        The Frobenius discriminant of E/F_q: t² - 4q, where t = tr π_E.

                        Instances For

                          The predicate that the Frobenius endomorphism is not an integer (i.e., t² ≠ 4q), so that ℤ[π_E] is a non-trivial quadratic order.

                          Instances For

                            The conductor of the order ℤ[π_E] inside the maximal quadratic order with discriminant frobDiscriminant E.

                            Instances For
                              noncomputable def OrdinarySupersingularClassification.endRingConductor {F : Type u_1} [Field F] [Fintype F] (E : WeierstrassCurve.Affine F) (hq : 0 < Fintype.card F) (hnotint : frobNotInt E) :

                              The conductor of the endomorphism ring of E inside the maximal quadratic order with discriminant frobDiscriminant E.

                              Instances For

                                The Frobenius order ℤ[π_E] is contained in the endomorphism ring End(E), expressed as a containment of the corresponding conductor orders.

                                The conductor of End(E) divides the conductor of ℤ[π_E], as a consequence of the order containment ℤ[π_E] ⊆ End(E).

                                The endomorphism ring is contained in the maximal order O_K (the conductor-1 order), since its conductor is a divisor of 1.

                                Theorem 13.8 of Sutherland: for an elliptic curve E/F_q whose geometric endomorphism algebra is an imaginary quadratic field K, the inclusions ℤ[π_E] ⊆ End(E) ⊆ O_K hold, and the conductor of End(E) divides [O_K : ℤ[π_E]].