Documentation

Atlas.EllipticCurves.code.Theorem136

The Frobenius discriminant $\Delta_\pi = t^2 - 4q \in \mathbb{Q}$, where $t$ is the trace of Frobenius and $q = \#F$ is the cardinality of the base finite field (Section 13.6).

Instances For
    noncomputable def EllipticCurve.endPoly {F : Type u} [Field F] [Fintype F] (W : WeierstrassCurve.Affine F) :

    The defining polynomial $X^2 - \Delta_\pi$ of the endomorphism algebra, where $\Delta_\pi = t^2 - 4q$ is the Frobenius discriminant. Adjoining a root yields an order in the imaginary quadratic field $\mathbb{Q}(\sqrt{\Delta_\pi})$.

    Instances For

      The polynomial $X^2 - \Delta_\pi$ is nonzero.

      The polynomial $X^2 - \Delta_\pi$ has degree $2 \neq 0$, which guarantees that AdjoinRoot (endPoly W) is nontrivial.

      The polynomial $X^2 - \Delta_\pi$ has natural degree $2$.

      noncomputable def EllipticCurve.EndAlgebra {F : Type u} [Field F] [Fintype F] (W : WeierstrassCurve.Affine F) :

      The endomorphism algebra $\mathrm{End}^0(E) = \mathbb{Q}[X]/(X^2 - \Delta_\pi)$ presented abstractly as the quotient algebra adjoining a square root of the Frobenius discriminant (Theorem 13.6).

      Instances For
        @[implicit_reducible]

        The endomorphism algebra inherits the commutative ring structure from AdjoinRoot.

        @[reducible]

        The (noncommutative) ring instance on the endomorphism algebra obtained by forgetting commutativity.

        @[reducible]

        The $\mathbb{Q}$-algebra structure on the endomorphism algebra inherited from AdjoinRoot.

        Since $\deg(X^2 - \Delta_\pi) \neq 0$, the endomorphism algebra is nontrivial.

        @[reducible]

        The endomorphism algebra is finite-dimensional over $\mathbb{Q}$: in fact it has dimension $2$ (cf. endAlg_finrank_eq_two), as $\mathrm{End}^0(E)$ is an imaginary quadratic field.

        The square root of the Frobenius discriminant $\sqrt{\Delta_\pi}$ inside the endomorphism algebra, realised as the adjoined root of $X^2 - \Delta_\pi$.

        Instances For

          The Frobenius endomorphism $\pi$ inside the endomorphism algebra, expressed as $\pi = t/2 + \sqrt{\Delta_\pi}/2$ where $t$ is the trace of Frobenius. This element satisfies $\pi^2 - t\pi + q = 0$ (Theorem 13.6, the characteristic polynomial of Frobenius).

          Instances For

            The defining relation $(\sqrt{\Delta_\pi})^2 = \Delta_\pi$ inside the endomorphism algebra, obtained directly from the polynomial $X^2 - \Delta_\pi$.

            The integer Frobenius discriminant $\Delta_\pi = t^2 - 4q$, where $t$ is the trace of Frobenius and $q = \#F$. By Hasse's bound this quantity is $\leq 0$ (Section 13.6).

            Instances For
              @[simp]

              Unfolding lemma: the Frobenius discriminant equals $t^2 - 4q$.

              The integer-valued and rational-valued Frobenius discriminants agree after coercion.

              The Hasse bound $|t| \leq 2\sqrt{q}$ implies $\Delta_\pi = t^2 - 4q \leq 0$.

              The condition that the Frobenius endomorphism $\pi$ is not an integer scalar, equivalently that $t^2 \neq 4q$, equivalently that $E/F$ is ordinary in the sense of Theorem 13.6.

              Instances For

                Combining frobeniusDiscriminant_nonpos with the non-integrality of Frobenius gives $\Delta_\pi < 0$, hence $\mathrm{End}^0(E)$ is an imaginary quadratic field.

                The rational Frobenius discriminant is strictly negative under the same hypotheses.

                $\dim_\mathbb{Q} \mathrm{End}^0(E) = 2$: the endomorphism algebra is a $2$-dimensional $\mathbb{Q}$-algebra, the imaginary quadratic field $\mathbb{Q}(\sqrt{\Delta_\pi})$ (part of Theorem 13.6).

                The endomorphism algebra contains an imaginary quadratic generator: an element $\alpha$ which is not a rational number and which squares to a negative rational. Witnesses the imaginary quadratic structure of $\mathrm{End}^0(E)$.

                The abstract endomorphism algebra of $E$ is ring-isomorphic to $\mathbb{Q}[X]/(X^2 - \Delta_\pi)$ (part of Theorem 13.6: identifies $\mathrm{End}^0(E)$ with $\mathbb{Q}(\sqrt{\Delta_\pi})$).

                Theorem 13.6 (combined statement). For an ordinary elliptic curve $E/F$ over a finite field: the Frobenius discriminant is negative, $\mathrm{End}^0(E)$ has $\mathbb{Q}$-dimension $2$, it contains an imaginary quadratic generator squaring to a negative rational, and it is isomorphic to $\mathbb{Q}[X]/(X^2 - \Delta_\pi)$.

                Concrete model: the endomorphism algebra is ring-isomorphic to the tensor product $\mathbb{Z}[\sqrt{\Delta_\pi}] \otimes_\mathbb{Z} \mathbb{Q}$, exhibiting it as the imaginary quadratic field $\mathbb{Q}(\sqrt{\Delta_\pi})$.