English
Let F be a separably closed field and E, E' be Weierstrass curves over F that are elliptic. If their j-invariants are equal, then there exists a VariableChange over F that maps E to E'.
Русский
Пусть F — отделимый замкнутый поля, E и E' — кривая Вейерштрасса над F, эллиптическая. Если их j-инварианты совпадают, то существует изменение переменных над F, переводящее E в E'.
LaTeX
$$$\exists C : \text{VariableChange } F,\ C \cdot E = E'$ при $E.j = E'.j$$$
Lean4
/-- If there are two elliptic curves with the same `j`-invariants defined over a
separably closed field, then there exists a change of variables over that field which change
one curve into another. -/
theorem exists_variableChange_of_j_eq (heq : E.j = E'.j) : ∃ C : VariableChange F, C • E = E' :=
by
obtain ⟨p, _⟩ := CharP.exists F
by_cases hchar2 : p = 2
· subst hchar2
exact exists_variableChange_of_char_two _ _ heq
by_cases hchar3 : p = 3
· subst hchar3
exact exists_variableChange_of_char_three _ _ heq
exact exists_variableChange_of_char_ne_two_or_three _ _ hchar2 hchar3 heq
