def shortWeierstrassCurve {k : Type u_1} [Field k] (A B : k) : WeierstrassCurve k

The short Weierstrass curve $y^2 = x^3 + Ax + B$, represented as the WeierstrassCurve with $a_1 = a_2 = a_3 = 0$, $a_4 = A$, and $a_6 = B$. Over fields of characteristic $\neq 2, 3$ every elliptic curve is isomorphic to one in this form.

def jInvariant {k : Type u_1} [Field k] (A B : k) : k

The $j$-invariant of a short Weierstrass curve $y^2 = x^3 + Ax + B$ (Definition 13.11): $j(A, B) = 1728 \cdot 4A^3 / (4A^3 + 27B^2)$.

@[simp]

theorem shortWeierstrassCurve_c₄ {k : Type u_1} [Field k] (A B : k) : (shortWeierstrassCurve A B).c₄ = -48 * A

For a short Weierstrass curve, the invariant $c_4$ simplifies to $-48 A$.

@[simp]

theorem shortWeierstrassCurve_Δ {k : Type u_1} [Field k] (A B : k) : (shortWeierstrassCurve A B).Δ = -16 * (4 * A ^ 3 + 27 * B ^ 2)

For a short Weierstrass curve, the discriminant simplifies to $\Delta = -16(4A^3 + 27B^2)$.

theorem four_ne_zero_of_two_ne_zero {k : Type u_1} [Field k] (h2 : 2 ≠ 0) : 4 ≠ 0

In a field where $2 \neq 0$, we also have $4 = 2^2 \neq 0$.

theorem sixteen_ne_zero_of_two_ne_zero {k : Type u_1} [Field k] (h2 : 2 ≠ 0) : 16 ≠ 0

In a field where $2 \neq 0$, we also have $16 = 2^4 \neq 0$.

theorem shortWeierstrassCurve_isElliptic {k : Type u_1} [Field k] (A B : k) (h2 : 2 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) : (shortWeierstrassCurve A B).IsElliptic

A short Weierstrass curve $y^2 = x^3 + Ax + B$ defines an elliptic curve provided $2 \neq 0$ and the discriminant condition $4A^3 + 27B^2 \neq 0$ holds.

theorem j_eq_jInvariant {k : Type u_1} [Field k] (A B : k) (h2 : 2 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) : (shortWeierstrassCurve A B).j = jInvariant A B

The Mathlib-defined $j$-invariant of a short Weierstrass curve agrees with the explicit formula jInvariant A B = 1728 \cdot 4A^3 / (4A^3 + 27B^2) of Definition 13.11.

@[simp]

theorem jInvariant_of_A_eq_zero {k : Type u_1} [Field k] (B : k) : jInvariant 0 B = 0

When $A = 0$, the $j$-invariant of $y^2 = x^3 + B$ is $0$.

theorem jInvariant_of_B_eq_zero {k : Type u_1} [Field k] (A : k) (hA : A ≠ 0) (h2 : 2 ≠ 0) : jInvariant A 0 = 1728

When $B = 0$ (and $A \neq 0$, $2 \neq 0$), the $j$-invariant of $y^2 = x^3 + Ax$ is exactly $1728$.

theorem twentyseven_ne_zero_of_three_ne_zero {k : Type u_1} [Field k] (h3 : 3 ≠ 0) : 27 ≠ 0

In a field where $3 \neq 0$, we also have $27 = 3^3 \neq 0$.

theorem onehundredeight_ne_zero {k : Type u_1} [Field k] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) : 108 ≠ 0

In a field where $2 \neq 0$ and $3 \neq 0$, we have $108 = 2^2 \cdot 3^3 \neq 0$.

theorem seventeentwentyeight_ne_zero {k : Type u_1} [Field k] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) : 1728 ≠ 0

In a field where $2 \neq 0$ and $3 \neq 0$, we have $1728 = 2^6 \cdot 3^3 \neq 0$.

theorem jInvariant_surjective {k : Type u_1} [Field k] (j₀ : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) : ∃ (A : k) (B : k), 4 * A ^ 3 + 27 * B ^ 2 ≠ 0 ∧ jInvariant A B = j₀

Theorem 13.12 (surjectivity of $j$): over any field of characteristic $\neq 2, 3$, every $j_0 \in k$ arises as the $j$-invariant of some short Weierstrass curve. The construction is explicit: $j_0 = 0$ uses $(A, B) = (0, 1)$, $j_0 = 1728$ uses $(1, 0)$, and otherwise $(3 j_0 (1728 - j_0), 2 j_0 (1728 - j_0)^2)$.

theorem short_weierstrass_iso_forward {k : Type u_1} [Field k] (A B A' B' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (C : WeierstrassCurve.VariableChange k) (hC : C • { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := A, a₆ := B } = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := A', a₆ := B' }) : C.s = 0 ∧ C.r = 0 ∧ C.t = 0 ∧ A' = ↑C.u⁻¹ ^ 4 * A ∧ B' = ↑C.u⁻¹ ^ 6 * B

Forward direction of the isomorphism classification (Theorem 13.13): any change of variables taking a short Weierstrass curve to another short Weierstrass curve must have $s = r = t = 0$, with the action on the coefficients given by $A' = u^{-4} A$ and $B' = u^{-6} B$.

theorem short_weierstrass_iso_backward {k : Type u_1} [Field k] (A B : k) (μ : kˣ) : { u := μ⁻¹, r := 0, s := 0, t := 0 } • { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := A, a₆ := B } = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := ↑μ ^ 4 * A, a₆ := ↑μ ^ 6 * B }

Backward direction of the isomorphism classification: for each unit $\mu \in k^\times$ the variable change with parameter $\mu^{-1}$ (and $r = s = t = 0$) takes $(A, B)$ to $(\mu^4 A, \mu^6 B)$.

theorem short_weierstrass_iso_iff {k : Type u_1} [Field k] (A B A' B' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) : (∃ (C : WeierstrassCurve.VariableChange k), C • { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := A, a₆ := B } = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := A', a₆ := B' }) ↔ ∃ (μ : kˣ), A' = ↑μ ^ 4 * A ∧ B' = ↑μ ^ 6 * B

Theorem 13.13 (isomorphism of short Weierstrass curves): two short Weierstrass curves are isomorphic over $k$ iff $(A', B') = (\mu^4 A, \mu^6 B)$ for some $\mu \in k^\times$.

theorem jInvariant_scaling {k : Type u_1} [Field k] (A B μ : k) (hμ : μ ≠ 0) : jInvariant (μ ^ 4 * A) (μ ^ 6 * B) = jInvariant A B

The $j$-invariant is scaling-invariant under $(A, B) \mapsto (\mu^4 A, \mu^6 B)$: this is the algebraic incarnation of the geometric isomorphism class invariance.

theorem A_eq_zero_of_jInvariant_eq_zero {k : Type u_1} [Field k] (A B : k) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hj : jInvariant A B = 0) : A = 0

If a nondegenerate short Weierstrass curve has $j = 0$ (in characteristic $\neq 2, 3$), then $A = 0$. This corresponds to the special locus of curves $y^2 = x^3 + B$.

theorem B_eq_zero_of_jInvariant_eq_1728 {k : Type u_1} [Field k] (A B : k) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hj : jInvariant A B = 1728) : B = 0

If a nondegenerate short Weierstrass curve has $j = 1728$ (in characteristic $\neq 2, 3$), then $B = 0$. This corresponds to the special locus of curves $y^2 = x^3 + Ax$.

theorem jInvariant_cross_multiply {k : Type u_1} [Field k] (A B A' B' : k) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) (hΔ' : 4 * A' ^ 3 + 27 * B' ^ 2 ≠ 0) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hj : jInvariant A B = jInvariant A' B') : A ^ 3 * (4 * A' ^ 3 + 27 * B' ^ 2) = A' ^ 3 * (4 * A ^ 3 + 27 * B ^ 2)

Cross-multiplying the equality $j(A, B) = j(A', B')$ on the $A$ side yields $A^3 \Delta' = A'^3 \Delta$ where $\Delta = 4A^3 + 27 B^2$.

theorem jInvariant_cross_multiply_B {k : Type u_1} [Field k] (A B A' B' : k) (h3 : 3 ≠ 0) (hjcross : A ^ 3 * (4 * A' ^ 3 + 27 * B' ^ 2) = A' ^ 3 * (4 * A ^ 3 + 27 * B ^ 2)) : B ^ 2 * (4 * A' ^ 3 + 27 * B' ^ 2) = B' ^ 2 * (4 * A ^ 3 + 27 * B ^ 2)

From the cross-multiplication identity for $A$, derive the analogous identity for $B$: $B^2 \Delta' = B'^2 \Delta$.

theorem jInvariant_converse_generic {k : Type u_1} [Field k] (A B A' B' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) (hΔ' : 4 * A' ^ 3 + 27 * B' ^ 2 ≠ 0) (hA : A ≠ 0) (hB : B ≠ 0) (hA' : A' ≠ 0) (hB' : B' ≠ 0) (hj : jInvariant A B = jInvariant A' B') : ∃ (u : k), u ≠ 0 ∧ A' = u ^ 2 * A ∧ B' = u ^ 3 * B

Generic case of the $j$-invariant converse: when $A, B, A', B' \neq 0$ and $j(A,B) = j(A',B')$, there exists $u \neq 0$ with $A' = u^2 A$ and $B' = u^3 B$. This produces the explicit isomorphism witness in the open locus $j \notin \{0, 1728\}$.

theorem jInvariant_eq_of_iso {k : Type u_1} [Field k] (A B A' B' μ : k) (hμ : μ ≠ 0) (hA' : A' = μ ^ 4 * A) (hB' : B' = μ ^ 6 * B) : jInvariant A B = jInvariant A' B'

If two short Weierstrass curves are related by the standard scaling $A' = \mu^4 A, B' = \mu^6 B$, then they have the same $j$-invariant.

theorem jInvariant_converse_ne_zero_ne_1728 {k : Type u_1} [Field k] (A B A' B' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) (hΔ' : 4 * A' ^ 3 + 27 * B' ^ 2 ≠ 0) (hj : jInvariant A B = jInvariant A' B') (hj0 : jInvariant A B ≠ 0) (hj1728 : jInvariant A B ≠ 1728) : ∃ (u : k), u ≠ 0 ∧ A' = u ^ 2 * A ∧ B' = u ^ 3 * B

Converse of equality of $j$-invariants in the generic case $j \neq 0, 1728$: deduces from $\Delta, \Delta' \neq 0$ and $j(A,B) = j(A',B')$ that all of $A, B, A', B'$ are nonzero, then applies jInvariant_converse_generic.

theorem jInvariant_converse_eq_zero {k : Type u_1} [Field k] (A B A' B' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) (hΔ' : 4 * A' ^ 3 + 27 * B' ^ 2 ≠ 0) (hj : jInvariant A B = jInvariant A' B') (hj0 : jInvariant A B = 0) : A = 0 ∧ A' = 0

If $j(A, B) = j(A', B') = 0$, then both $A$ and $A'$ are zero (special locus of $j = 0$).

theorem jInvariant_converse_eq_1728 {k : Type u_1} [Field k] (A B A' B' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) (hΔ' : 4 * A' ^ 3 + 27 * B' ^ 2 ≠ 0) (hj : jInvariant A B = jInvariant A' B') (hj1728 : jInvariant A B = 1728) : B = 0 ∧ B' = 0

If $j(A, B) = j(A', B') = 1728$, then both $B$ and $B'$ are zero (special locus of $j = 1728$).

theorem jInvariant_algebraMap {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra k K] (A B : k) : (algebraMap k K) (jInvariant A B) = jInvariant ((algebraMap k K) A) ((algebraMap k K) B)

The $j$-invariant is preserved under base change along any field extension $K/k$: $\mathrm{alg.map}(j(A, B)) = j(\mathrm{alg.map}(A), \mathrm{alg.map}(B))$.

theorem minpoly_natDegree_le_of_pow_eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (μ : K) (a : k) (n : ℕ) (hn : 0 < n) (hμ : μ ^ n = (algebraMap k K) a) : (minpoly k μ).natDegree ≤ n

If $\mu \in K$ satisfies $\mu^n = a$ for some $a \in k$ and $n > 0$, then $\mu$ is algebraic over $k$ of degree at most $n$ (since $X^n - a$ is a degree-$n$ annihilating polynomial).

theorem isomorphic_over_algClosure_iff_jInvariant_eq {k : Type u_1} [Field k] (A B A' B' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hΔ : 4 * A ^ 3 + 27 * B ^ 2 ≠ 0) (hΔ' : 4 * A' ^ 3 + 27 * B' ^ 2 ≠ 0) : (∃ (μ : AlgebraicClosure k), μ ≠ 0 ∧ (algebraMap k (AlgebraicClosure k)) A' = μ ^ 4 * (algebraMap k (AlgebraicClosure k)) A ∧ (algebraMap k (AlgebraicClosure k)) B' = μ ^ 6 * (algebraMap k (AlgebraicClosure k)) B) ↔ jInvariant A B = jInvariant A' B'

Theorem 13.14 (isomorphism over the algebraic closure): two short Weierstrass curves $E_{A,B}$ and $E_{A',B'}$ over $k$ become isomorphic over $\overline{k}$ iff they have the same $j$-invariant. The isomorphism is via $(A', B') = (\mu^4 A, \mu^6 B)$ for some $\mu \in \overline{k}^\times$.