Instances For
- is_morphism : IsMorphismOfCurves self.toFun
- surjective : Function.Surjective self.toFun
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Corollary: the kernel preimage $\varphi^{-1}\{0\}$ of an isogeny is a finite set.
The kernel subgroup $\ker \varphi$, viewed as a set in $E_1(F)$, is finite.
The function-field extension data associated to an isogeny $\varphi$: a pair of fields $k(E_1) \supseteq \varphi^* k(E_2)$ with the inclusion as an algebra map.
- FunctionField : Type
- PullbackField : Type
- field_top : Field self.FunctionField
- field_bot : Field self.PullbackField
- algebra_inst : Algebra self.PullbackField self.FunctionField
Instances For
The "top" field $k(E_1)$ is a field.
The "bottom" field $\varphi^* k(E_2)$ is a field.
$k(E_1)$ is an algebra over the pullback field $\varphi^* k(E_2)$.
An isogeny is separable if the induced function-field extension is separable.
Instances For
An isogeny is inseparable if it fails to be separable.
Instances For
An isogeny is purely inseparable if the induced function-field extension is purely inseparable.
Instances For
An isogeny respects negation: $\varphi(-P) = -\varphi(P)$ (corollary of being a group homomorphism).
Auxiliary: the underlying isogeny built by base-changing $\varphi$ along
$k \to L$, packaged from hasMapOnPoints.
Instances For
The base change $\varphi_L : E_{1,L} \to E_{2,L}$ of an isogeny $\varphi$ along a field extension $k \to L$.
Instances For
The base-changed isogeny is also additive on points over the extension.
The base-changed isogeny as a group homomorphism over $L$.
Instances For
Encode an affine Weierstrass point as Option (R × R): the point at infinity is
none, and an affine point $(x, y)$ is some (x, y).
Instances For
The encoding toOption is injective: distinct affine points have distinct
encodings.
If the base ring is finite, then the set of points of an affine Weierstrass curve is also finite.
In a torsion-free abelian group, an element of finite additive order must be zero.
An elliptic curve over $\mathbb{Q}$ has good reduction at a prime $p$ if it admits a model that reduces mod $p$ to an elliptic curve over $\mathbb{F}_p$.
- reducedCurve : WeierstrassCurve (ZMod p)
- isElliptic : self.reducedCurve.IsElliptic
Instances For
Theorem 24.14: the reduction-mod-$p$ map $E(\mathbb{Q}) \to \tilde E(\mathbb{F}_p)$ on points, as a group homomorphism, for an elliptic curve with good reduction at $p$.
Instances For
Corollary 24.18: the kernel of the reduction-mod-$p$ map is torsion-free, hence contains no nontrivial finite-order points.
Combined statement: existence of a reduction-mod-$p$ map whose kernel is torsion-free.
Corollary: the reduction map restricted to the torsion subgroup of $E(\mathbb{Q})$ is injective into $\tilde E(\mathbb{F}_p)$ for any prime $p$ of good reduction.
A nonsingular point $(x_0, y_0)$ on a short Weierstrass curve $y^2 = x^3 + a_4 x + a_6$ satisfies the curve equation.
A rational number with nonnegative $p$-adic valuation at every prime is an integer.
If a torsion point on a short Weierstrass curve over $\mathbb{Q}$ with integral coefficients has rational coordinates, then its $x$-coordinate has nonnegative $p$-adic valuation at every prime $p$.
First part of Nagell-Lutz: any rational torsion point on a short Weierstrass curve $E/\mathbb{Q}$ with integer coefficients has integer coordinates $(x_0, y_0) \in \mathbb{Z}^2$.
Slope-divisibility step of Nagell-Lutz: if $(x_0, y_0)$ is an integral torsion point on the short Weierstrass curve with $y_0 \neq 0$, then $y_0^2 \mid (3 x_0^2 + a_4)^2$.
Theorem 24.21 (Nagell-Lutz): any rational torsion point $(x_0, y_0)$ on the short Weierstrass curve $y^2 = x^3 + a_4 x + a_6$ over $\mathbb{Q}$ (with $a_4, a_6 \in \mathbb{Z}$) satisfies $x_0, y_0 \in \mathbb{Z}$, and either $y_0 = 0$ or $y_0^2 \mid (4 a_4^3 + 27 a_6^2)$.
Axiom: a nonconstant morphism of curves $f : E \to E$ sending $0$ to $0$ is surjective (a curve of genus one has no nontrivial subvariety of dimension one).
Axiom: for any $n > 0$, the multiplication-by-$n$ map on an elliptic curve has a nonzero image, i.e. it is not the zero map.
For any $n > 0$, multiplication-by-$n$ is a morphism of curves $E \to E$
(proved by induction using isMorphismOfCurves_add).
Multiplication-by-$n$ on $E$ is surjective for $n > 0$ (combining nonconstancy
and isMorphismOfCurves_nonconstant_surjective).
Restatement of mulByN_surjective_axiom for use inside the
Theorem248 section.
Theorem 24.8: the multiplication-by-$n$ map $[n] : E \to E$ is an isogeny of elliptic curves for every $n > 0$.
Instances For
Corollary 24.10: the $n$-torsion subgroup $E[n] \subseteq E(F)$ is finite.
Variant of Corollary 24.10 over an algebraic closure: $E(\bar k)[n]$ is finite.
The base change of an elliptic curve $E/\mathbb{Q}$ to $\mathbb{Q}_p$ remains elliptic (its discriminant remains a unit).
Membership in the $n$-th piece of the $p$-adic filtration on $E(\mathbb{Q}_p)$: the point $O$ is always in, and an affine point $(x, y)$ lies in $E_n$ when $n = 0$ or when $y \neq 0$ and $v_p(x) - v_p(y) \geq n$.
Instances For
The identity point lies in every piece $E_n$ of the $p$-adic filtration.
The filtration is monotone: if $P \in E_n$ and $m \leq n$, then $P \in E_m$.
The $p$-adic filtration on $E(\mathbb{Q}_p)$: a decreasing family of subgroups $E = E_0 \supseteq E_1 \supseteq E_2 \supseteq \cdots$ defined via the $p$-adic valuation, together with the (mild) assumptions $a_1 = a_2 = a_3 = 0$ required for the addition-formula computations.
- group : ℕ → AddSubgroup (W.baseChange ℚ_[p]).toAffine.Point
- mem_iff (n : ℕ) (P : (W.baseChange ℚ_[p]).toAffine.Point) : P ∈ self.group n ↔ PadicFiltrationMem W p n P
Instances For
The $n$-th level $E_n$ of the $p$-adic filtration is closed under addition: if $P, Q \in E_n$ then $P + Q \in E_n$.
The $n$-th level $E_n$ of the $p$-adic filtration is closed under negation: if $P \in E_n$ then $-P \in E_n$.
The $n$-th level $E_n$ of the $p$-adic filtration, packaged as an additive subgroup of $E(\mathbb{Q}_p)$.
Instances For
Existence of the $p$-adic filtration on $E(\mathbb{Q}_p)$ for a Weierstrass curve with $a_1 = a_2 = a_3 = 0$.
If reduction modulo $p$ is surjective on $E(\mathbb{Q}_p)$, then it remains surjective when restricted to $E_0 = E(\mathbb{Q}_p)$.
The reduction map $\rho: E_0 \to \widetilde{E}(\mathbb{F}_p)$ is surjective with kernel $E_1$.
The first isomorphism theorem applied to the reduction map gives $E_0/E_1 \cong \widetilde{E}(\mathbb{F}_p)$.
For $n > 0$, the predicate PadicFiltrationMem agrees with the
PadicElliptic.InPadicFiltration predicate from the formal-group development.
For $n > 0$, the subgroup $E_n$ of the filtration coincides with the
$n$-th level of PadicElliptic.padicFiltration.
For $n > 0$, the formal logarithm provides a surjective homomorphism $E_n \to \mathbb{F}_p$ with kernel $E_{n+1}$.
For $n > 0$, the successive quotient of the filtration is isomorphic to $\mathbb{F}_p$: $E_n / E_{n+1} \cong \mathbb{F}_p$.
The $p$-adic filtration is separated: $\bigcap_{n \geq 0} E_n = 0$.
Theorem 24.14 (Reduction theorem for the $p$-adic filtration). The successive quotients of $E_0 \supseteq E_1 \supseteq E_2 \supseteq \cdots$ are: \begin{itemize} \item $E_0/E_1 \cong \widetilde{E}(\mathbb{F}_p)$ (reduction modulo $p$), \item $E_n/E_{n+1} \cong \mathbb{F}_p$ for all $n \geq 1$ (via the formal logarithm), \item $\bigcap_n E_n = 0$ (the filtration is separated). \end{itemize}
Predicate: an affine point $P = (x, y) \in E(\mathbb{Q}_p)$ has $p$-adically integral coordinates, i.e. $v_p(x) \geq 0$ and $v_p(y) \geq 0$ (the point at infinity is vacuously integral).
Instances For
Valuation bound from the Weierstrass equation: if the coefficients $a_i$ are $p$-integral and the point $(x, y)$ on $E$ does not have integral coordinates, then $y \neq 0$ and $v_p(x) - v_p(y) \geq 1$.
A point with non-integral coordinates lies in $E_1$ (in fact in some $E_n$ with $n > 0$) but does not lie in every $E_k$, since the filtration is separated.
Corollary 24.16. Let $E$ be an elliptic curve over $\mathbb{Q}$ with $p$-integral Weierstrass coefficients, and let $P \in E(\mathbb{Q}_p)$. If $m \cdot P = 0$ for some integer $m$ with $\gcd(m, p) = 1$, then the coordinates of $P$ are $p$-adically integral.