def shortWeierstrassCurve {R : Type u_1} [CommRing R] (a₄ a₆ : R) : WeierstrassCurve R

The Weierstrass curve in short form $y^2 = x^3 + a_4 x + a_6$, obtained by setting $a_1 = a_2 = a_3 = 0$.

@[simp]

theorem shortWeierstrassCurve.a₁_eq {R : Type u_1} [CommRing R] (a₄ a₆ : R) : (shortWeierstrassCurve a₄ a₆).a₁ = 0

Coefficient $a_1$ of the short Weierstrass curve is $0$.

@[simp]

theorem shortWeierstrassCurve.a₂_eq {R : Type u_1} [CommRing R] (a₄ a₆ : R) : (shortWeierstrassCurve a₄ a₆).a₂ = 0

Coefficient $a_2$ of the short Weierstrass curve is $0$.

@[simp]

theorem shortWeierstrassCurve.a₃_eq {R : Type u_1} [CommRing R] (a₄ a₆ : R) : (shortWeierstrassCurve a₄ a₆).a₃ = 0

Coefficient $a_3$ of the short Weierstrass curve is $0$.

@[simp]

theorem shortWeierstrassCurve.a₄_eq {R : Type u_1} [CommRing R] (a₄ a₆ : R) : (shortWeierstrassCurve a₄ a₆).a₄ = a₄

Coefficient $a_4$ of the short Weierstrass curve is $a_4$.

@[simp]

theorem shortWeierstrassCurve.a₆_eq {R : Type u_1} [CommRing R] (a₄ a₆ : R) : (shortWeierstrassCurve a₄ a₆).a₆ = a₆

Coefficient $a_6$ of the short Weierstrass curve is $a_6$.

theorem shortWeierstrassCurve.c₄_eq {R : Type u_1} [CommRing R] (a₄ a₆ : R) : (shortWeierstrassCurve a₄ a₆).c₄ = -48 * a₄

For a short Weierstrass curve, the auxiliary invariant $c_4 = -48 a_4$.

theorem shortWeierstrassCurve.c₆_eq {R : Type u_1} [CommRing R] (a₄ a₆ : R) : (shortWeierstrassCurve a₄ a₆).c₆ = -864 * a₆

For a short Weierstrass curve, the auxiliary invariant $c_6 = -864 a_6$.

theorem shortWeierstrassCurve.Δ_eq {R : Type u_1} [CommRing R] (a₄ a₆ : R) : (shortWeierstrassCurve a₄ a₆).Δ = -16 * (4 * a₄ ^ 3 + 27 * a₆ ^ 2)

The discriminant of the short Weierstrass curve: $\Delta = -16(4 a_4^3 + 27 a_6^2)$.

theorem WeierstrassCurve.j_mul_Δ_eq_c₄_cube {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : W.j * W.Δ = W.c₄ ^ 3

The defining relation $j \cdot \Delta = c_4^3$ for the $j$-invariant of an elliptic Weierstrass curve.

theorem shortWeierstrassCurve.sixteen_ne_zero {F : Type u_1} [Field F] (a₄ a₆ : F) [(shortWeierstrassCurve a₄ a₆).IsElliptic] : 16 ≠ 0

Over a field, if the short Weierstrass curve $y^2 = x^3 + a_4 x + a_6$ is elliptic, then $16 \neq 0$ (i.e. the characteristic is not $2$).

theorem shortWeierstrassCurve.denominator_ne_zero {F : Type u_1} [Field F] (a₄ a₆ : F) [(shortWeierstrassCurve a₄ a₆).IsElliptic] : 4 * a₄ ^ 3 + 27 * a₆ ^ 2 ≠ 0

For an elliptic short Weierstrass curve, the quantity $4 a_4^3 + 27 a_6^2 \neq 0$ (it is essentially the discriminant up to a unit).

theorem j_invariant_short_weierstrass_eq {F : Type u_1} [Field F] (a₄ a₆ : F) [(shortWeierstrassCurve a₄ a₆).IsElliptic] : (shortWeierstrassCurve a₄ a₆).j = 1728 * (4 * a₄ ^ 3) / (4 * a₄ ^ 3 + 27 * a₆ ^ 2)

Closed form for the $j$-invariant of a short Weierstrass curve: $j = 1728 \cdot \dfrac{4 a_4^3}{4 a_4^3 + 27 a_6^2}$.

noncomputable def EllipticCurveOver.jInvariant {k : Type u_1} [Field k] (E : EllipticCurveOver k) : k

Definition 26.1. The $j$-invariant of an elliptic curve $E$ over a field $k$, extracted from its underlying Weierstrass curve.

theorem j_invariant_surjective {k : Type u_1} [Field k] (j : k) : ∃ (E : EllipticCurveOver k), E.jInvariant = j

Theorem 26.3 (surjectivity). Over any field $k$, every value $j \in k$ arises as the $j$-invariant of some elliptic curve over $k$.

noncomputable def ellipticCurveOfJ {k : Type u_1} [Field k] (j : k) : EllipticCurveOver k

A choice of elliptic curve over $k$ whose $j$-invariant equals $j$, witnessing the surjectivity of the $j$-invariant.

theorem ellipticCurveOfJ_jInvariant {k : Type u_1} [Field k] (j : k) : (ellipticCurveOfJ j).jInvariant = j

The chosen curve ellipticCurveOfJ j indeed has $j$-invariant $j$.

theorem j_invariant_surjective_fun {k : Type u_1} [Field k] : Function.Surjective EllipticCurveOver.jInvariant

Surjectivity of the $j$-invariant function $E \mapsto j(E)$ on elliptic curves over $k$, restated as Function.Surjective.

def GenusOneCurve.jacobian {k : Type u_1} [Field k] (C : GenusOneCurve k) : EllipticCurveOver k

The Jacobian of a genus-one curve $C$, viewed as an elliptic curve over $k$.

noncomputable def GenusOneCurve.Pic0GroupType {k : Type u_2} [Field k] : GenusOneCurve k → Type u_3

The underlying type carrying $\mathrm{Pic}^0(C)$, the degree-zero Picard group of a genus-one curve $C$ over $k$.

def GenusOneCurve.Pic0Group {k : Type u_2} [Field k] (C : GenusOneCurve k) : Type u_3

The degree-zero Picard group $\mathrm{Pic}^0(C)$ of a genus-one curve $C$.

@[implicit_reducible]

noncomputable instance GenusOneCurve.Pic0Group.instAddCommGroupAxiom {k : Type u_2} [Field k] (C : GenusOneCurve k) : AddCommGroup C.Pic0Group

Axiom providing the abelian group structure on $\mathrm{Pic}^0(C)$.

@[implicit_reducible]

noncomputable instance GenusOneCurve.Pic0Group.instAddCommGroup {k : Type u_2} [Field k] (C : GenusOneCurve k) : AddCommGroup C.Pic0Group

Bundled abelian group instance on $\mathrm{Pic}^0(C)$.

def EllipticCurveOver.RationalPoints {k : Type u_1} [Field k] (E : EllipticCurveOver k) : Type u_1

The group of $k$-rational points $E(k)$ of an elliptic curve $E$ over $k$, defined as the affine points of its underlying Weierstrass curve.

theorem EllipticCurveOver.RationalPoints_def {k : Type u_1} [Field k] (E : EllipticCurveOver k) : E.RationalPoints = E.curve.toAffine.Point

Definitional unfolding: $E(k)$ is the affine points of the underlying Weierstrass curve.

@[implicit_reducible]

noncomputable instance EllipticCurveOver.RationalPoints.instAddCommGroup {k : Type u_1} [Field k] (E : EllipticCurveOver k) : AddCommGroup E.RationalPoints

The Mordell–Weil abelian group structure on $E(k)$.

noncomputable def GenusOneCurve.pic0_iso_jacobian {k : Type u_1} [Field k] (C : GenusOneCurve k) : C.Pic0Group ≃+ C.jacobian.RationalPoints

The canonical isomorphism $\mathrm{Pic}^0(C) \cong J(C)(k)$ identifying the degree-zero Picard group of a genus-one curve with the $k$-rational points of its Jacobian.

def LocalWCProduct {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) : Type (u + 1)

The product $\prod_v \mathrm{WC}(E/k_v)$ of local Weil–Châtelet groups over all places $v$ of the number field $k$.

@[reducible]

noncomputable def LocalWCProduct.instAddCommGroupAxiom {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) : AddCommGroup (LocalWCProduct E)

The componentwise abelian group structure on LocalWCProduct E, inherited from the pointwise product of local Weil–Châtelet groups.

@[implicit_reducible]

noncomputable instance LocalWCProduct.instAddCommGroup {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) : AddCommGroup (LocalWCProduct E)

Bundled abelian group instance on LocalWCProduct E.

noncomputable def WeilChateletGroup.localizationMapAxiom {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) : WeilChateletGroup E →+ LocalWCProduct E

The localization homomorphism $\mathrm{WC}(E/k) \to \prod_v \mathrm{WC}(E/k_v)$ assembled from the place-by-place localization maps.

noncomputable def WeilChateletGroup.localizationMap {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) : WeilChateletGroup E →+ LocalWCProduct E

The global-to-local restriction homomorphism on Weil–Châtelet groups, sending $\xi \in \mathrm{WC}(E/k)$ to the tuple of its images $(\xi_v)_v$.

noncomputable def TateShafarevich.asKernel {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) : AddSubgroup (WeilChateletGroup E)

The Tate–Shafarevich group $Ш(E/k)$ realised as a subgroup of $\mathrm{WC}(E/k)$: the kernel of the localization map.

theorem TateShafarevich.range_eq_ker_axiom {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) : (toWC E).range = asKernel E

The range of the embedding $Ш(E/k) \hookrightarrow \mathrm{WC}(E/k)$ equals the kernel of the localization map, providing the kernel description of the Tate–Shafarevich group.

theorem TateShafarevich.range_eq_ker {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) : (toWC E).range = asKernel E

User-facing form of TateShafarevich.range_eq_ker_axiom: the image of $Ш(E/k)$ in $\mathrm{WC}(E/k)$ is exactly the kernel of the localization map.

theorem mem_tateShafarevich_asKernel_iff {k : Type u} [Field k] [NumberField k] (E : EllipticCurveOver k) (x : WeilChateletGroup E) : x ∈ TateShafarevich.asKernel E ↔ (WeilChateletGroup.localizationMap E) x = 0

Membership criterion: $x \in Ш(E/k)$ iff its image under the localization map is zero.

def GenusOneCurve.PointOverAlgClosure {k : Type u} [Field k] (C : GenusOneCurve k) : Type u

The set of $\bar k$-rational points of the Jacobian of $C$, used as base points for the elliptic-curve structure of $C \otimes_k \bar k$.

theorem GenusOneCurve.PointOverAlgClosure.nonempty {k : Type u} [Field k] (C : GenusOneCurve k) : Nonempty C.PointOverAlgClosure

The set of $\bar k$-rational points of the Jacobian is nonempty, witnessed by the identity element.

noncomputable def GenusOneCurve.ellipticCurveAtBasePoint {k : Type u} [Field k] (C : GenusOneCurve k) (O : C.PointOverAlgClosure) : EllipticCurveOver (AlgebraicClosure k)

Given a $\bar k$-point $O$ of $C$, the associated elliptic curve over $\bar k$ obtained by translating the Weierstrass model so that $O$ becomes the identity.

instance EllipticCurveOver.instIsElliptic {k : Type u_1} [Field k] (E : EllipticCurveOver k) : E.curve.IsElliptic

An elliptic curve bundles an IsElliptic instance on its underlying Weierstrass curve, registered for typeclass search.

theorem GenusOneCurve.translationIsomorphism {k : Type u} [Field k] (C : GenusOneCurve k) (O O' : C.PointOverAlgClosure) : ∃ (σ : WeierstrassCurve.VariableChange (AlgebraicClosure k)), (C.ellipticCurveAtBasePoint O').curve = σ • (C.ellipticCurveAtBasePoint O).curve

Changing the base point $O \mapsto O'$ on a genus-one curve $C$ yields an isomorphism of the associated elliptic curves over $\bar k$ via an explicit Weierstrass variable change.

theorem GenusOneCurve.jInvariant_eq_of_basePoints {k : Type u} [Field k] (C : GenusOneCurve k) (O O' : C.PointOverAlgClosure) : (C.ellipticCurveAtBasePoint O).jInvariant = (C.ellipticCurveAtBasePoint O').jInvariant

The $j$-invariant of the elliptic curve $C_O$ associated to $C$ at a base point $O$ is independent of the choice of base point.

noncomputable def GenusOneCurve.jInvariant {k : Type u} [Field k] (C : GenusOneCurve k) : k

The $j$-invariant $j(C) \in k$ of a genus-one curve $C$, defined as the $j$-invariant of its Jacobian.

@[simp]

theorem GenusOneCurve.jInvariant_eq_jacobian_jInvariant {k : Type u} [Field k] (C : GenusOneCurve k) : C.jInvariant = C.Jacobian.jInvariant

Definitional unfolding: $j(C) = j(\mathrm{Jac}(C))$.

theorem j_eq_of_isomorphic_over_closure {k : Type u_1} [Field k] (W₁ W₂ : WeierstrassCurve k) [W₁.IsElliptic] [W₂.IsElliptic] (h : ∃ (C : WeierstrassCurve.VariableChange (AlgebraicClosure k)), C • W₁.baseChange (AlgebraicClosure k) = W₂.baseChange (AlgebraicClosure k)) : W₁.j = W₂.j

Theorem 26.4 ($\Rightarrow$). If $W_1$ and $W_2$ become isomorphic over the algebraic closure $\bar k$, then they have the same $j$-invariant.

theorem isomorphic_over_closure_of_j_eq {k : Type u_1} [Field k] (W₁ W₂ : WeierstrassCurve k) [W₁.IsElliptic] [W₂.IsElliptic] (hj : W₁.j = W₂.j) : ∃ (C : WeierstrassCurve.VariableChange (AlgebraicClosure k)), C • W₁.baseChange (AlgebraicClosure k) = W₂.baseChange (AlgebraicClosure k)

Theorem 26.4 ($\Leftarrow$). If two elliptic Weierstrass curves over $k$ share the same $j$-invariant, they become isomorphic after base change to $\bar k$.

theorem j_invariant_iff_isomorphic_over_closure {k : Type u_1} [Field k] (W₁ W₂ : WeierstrassCurve k) [W₁.IsElliptic] [W₂.IsElliptic] : W₁.j = W₂.j ↔ ∃ (C : WeierstrassCurve.VariableChange (AlgebraicClosure k)), C • W₁.baseChange (AlgebraicClosure k) = W₂.baseChange (AlgebraicClosure k)

Theorem 26.4. Two elliptic Weierstrass curves over $k$ have equal $j$-invariant if and only if they become isomorphic over the algebraic closure $\bar k$.