theorem algebraMap_AlgClosure_ne_zero {k : Type u} [Field k] (a : k) (ha : a ≠ 0) : (algebraMap k (AlgebraicClosure k)) a ≠ 0

The image of a nonzero element of $k$ under the canonical inclusion $k \hookrightarrow \overline{k}$ remains nonzero.

theorem lemma_26_9_cross_identity {k : Type u} [Field k] (a₄ a₆ a₄' a₆' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hΔ : 4 * a₄ ^ 3 + 27 * a₆ ^ 2 ≠ 0) (hΔ' : 4 * a₄' ^ 3 + 27 * a₆' ^ 2 ≠ 0) (hj : 1728 * (4 * a₄ ^ 3) / (4 * a₄ ^ 3 + 27 * a₆ ^ 2) = 1728 * (4 * a₄' ^ 3) / (4 * a₄' ^ 3 + 27 * a₆' ^ 2)) : a₆' ^ 2 * a₄ ^ 3 = a₆ ^ 2 * a₄' ^ 3

Cross-multiplication identity following from equality of $j$-invariants of two short Weierstrass curves: $a_6'^2 a_4^3 = a_6^2 a_4'^3$. A key algebraic step in Lemma 26.9.

theorem a₄'_ne_zero_of_generic {k : Type u} [Field k] (a₄ a₆ a₄' a₆' : k) (ha₄ : a₄ ≠ 0) (_ha₆ : a₆ ≠ 0) (hΔ' : 4 * a₄' ^ 3 + 27 * a₆' ^ 2 ≠ 0) (hcross : a₆' ^ 2 * a₄ ^ 3 = a₆ ^ 2 * a₄' ^ 3) : a₄' ≠ 0

In the "generic" case where both $a_4$ and $a_6$ are nonzero, the cross identity forces $a_4' \neq 0$.

theorem a₆'_ne_zero_of_generic {k : Type u} [Field k] (a₄ a₆ a₄' a₆' : k) (_ha₄ : a₄ ≠ 0) (ha₆ : a₆ ≠ 0) (hΔ' : 4 * a₄' ^ 3 + 27 * a₆' ^ 2 ≠ 0) (hcross : a₆' ^ 2 * a₄ ^ 3 = a₆ ^ 2 * a₄' ^ 3) : a₆' ≠ 0

In the "generic" case where both $a_4$ and $a_6$ are nonzero, the cross identity forces $a_6' \neq 0$.

theorem a₆'_zero_of_a₆_zero {k : Type u} [Field k] (a₄ a₆ a₄' a₆' : k) (ha₆ : a₆ = 0) (ha₄ : a₄ ≠ 0) (hcross : a₆' ^ 2 * a₄ ^ 3 = a₆ ^ 2 * a₄' ^ 3) : a₆' = 0

Boundary case: if $a_6 = 0$ and $a_4 \neq 0$, then $a_6' = 0$.

theorem a₄'_zero_of_a₄_zero {k : Type u} [Field k] (a₄ a₆ a₄' a₆' : k) (ha₄ : a₄ = 0) (ha₆ : a₆ ≠ 0) (hcross : a₆' ^ 2 * a₄ ^ 3 = a₆ ^ 2 * a₄' ^ 3) : a₄' = 0

Boundary case: if $a_4 = 0$ and $a_6 \neq 0$, then $a_4' = 0$.

theorem lemma_26_9 {k : Type u} [Field k] (a₄ a₆ a₄' a₆' : k) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hΔ : 4 * a₄ ^ 3 + 27 * a₆ ^ 2 ≠ 0) (hΔ' : 4 * a₄' ^ 3 + 27 * a₆' ^ 2 ≠ 0) (hj : 1728 * (4 * a₄ ^ 3) / (4 * a₄ ^ 3 + 27 * a₆ ^ 2) = 1728 * (4 * a₄' ^ 3) / (4 * a₄' ^ 3 + 27 * a₆' ^ 2)) : ∃ (l : AlgebraicClosure k), l ≠ 0 ∧ (algebraMap k (AlgebraicClosure k)) a₄' = l ^ 4 * (algebraMap k (AlgebraicClosure k)) a₄ ∧ (algebraMap k (AlgebraicClosure k)) a₆' = l ^ 6 * (algebraMap k (AlgebraicClosure k)) a₆

Lemma 26.9. Two short Weierstrass curves over $k$ with equal $j$-invariant become isomorphic over $\overline{k}$ via a scalar twist: there exists $\lambda \in \overline{k}^\times$ with $a_4' = \lambda^4 a_4$ and $a_6' = \lambda^6 a_6$.