theorem Polynomial.derivative_eq_zero_of_sq {k : Type u_1} [Field k] (hp2 : 2 ≠ 0) {t : Polynomial k} (ht : t ≠ 0) (h : derivative (t ^ 2) = 0) : derivative t = 0

Over a field in which 2 ≠ 0, if t is nonzero and (t^2)' = 0, then t' = 0. Used in characteristic-p arguments where vanishing of the derivative of a square forces vanishing of the derivative of the base polynomial.

theorem wronskian_from_curve_eq {k : Type u_1} [Field k] {v s t f₁ w : Polynomial k} (hv_ne : v ≠ 0) (hcurve : v ^ 3 * s ^ 2 * f₁ = t ^ 2 * w) (hv' : Polynomial.derivative v = 0) (hw' : Polynomial.derivative w = 0) : (s ^ 2 * f₁).wronskian (t ^ 2) = 0

From the curve equation v³ · s² · f₁ = t² · w of an isogeny in standard form, together with v' = 0 and w' = 0, deduce that the Wronskian of s² · f₁ and t² vanishes. A key computation in the proof of Lemma 5.3.

theorem lemma_5_3_x {k : Type u_1} [Field k] {p : ℕ} [CharP k p] (hp : p ≠ 0) {u v : Polynomial k} (hcop : IsCoprime u v) (hinsep : Polynomial.derivative u * v - u * Polynomial.derivative v = 0) : ∃ (f : Polynomial k) (g : Polynomial k), (Polynomial.expand k p) f = u ∧ (Polynomial.expand k p) g = v

The "x-coordinate" part of Lemma 5.3: in characteristic p > 0, if coprime polynomials u, v satisfy u'v - uv' = 0 (inseparability of u/v), then u and v are both p-th powers, i.e. of the form f(x^p) and g(x^p). This corresponds to Lemma 5.1 applied to the x-coordinate of an inseparable isogeny.

theorem coprime_s2f1_t2 {k : Type u_1} [Field k] {s t f₁ : Polynomial k} (hcop_st : IsCoprime s t) (hcop_ft : IsCoprime f₁ t) : IsCoprime (s ^ 2 * f₁) (t ^ 2)

If s and t are coprime and f₁ and t are coprime, then s² · f₁ is coprime to t². A bookkeeping lemma supporting the curve equation analysis.

theorem dvd_of_dvd_mul_isUnit_poly {k : Type u_1} [Field k] {a b c : Polynomial k} (hu : IsUnit a) (h : c ∣ a * b) : c ∣ b

If a is a unit in k[X] and c ∣ a · b, then c ∣ b. A small divisibility lemma used to peel off unit constants in characteristic-p arguments.

theorem sep_dvd_of_deriv_sq_mul_pow {k : Type u_1} [Field k] {r f₁ : Polynomial k} {m : ℕ} (hm : m > 0) (hCm : ↑m ≠ 0) (hf₁_sep : f₁.Separable) (h_deriv : Polynomial.derivative (r ^ 2 * f₁ ^ m) = 0) : f₁ ∣ r

If f₁ is separable, m > 0, m ≠ 0 in k, and (r² · f₁^m)' = 0, then f₁ ∣ r. This is the inductive step extracting more f₁ factors from s in the proof of the y-coordinate part of Lemma 5.3.

theorem insep_y_factor {k : Type u_1} [Field k] {p : ℕ} [CharP k p] (hp : p ≠ 0) (hp2 : 2 ≠ 0) {s f₁ : Polynomial k} (hs : s ≠ 0) (hf₁_sep : f₁.Separable) (h_deriv : Polynomial.derivative (s ^ 2 * f₁) = 0) : ∃ (g₂ : Polynomial k), s ^ 2 * f₁ = (Polynomial.expand k p) g₂ ^ 2 * f₁ ^ p

The "y-coordinate" factorization of Lemma 5.3: in characteristic p > 0, if f₁ is separable, s ≠ 0, and (s² · f₁)' = 0, then s² · f₁ = (expand_p g₂)² · f₁^p for some g₂. This shows the y-coefficient of an inseparable isogeny is a p-th power times the suitable factor of f₁.

theorem lemma_5_3_y_deriv_t {k : Type u_1} [Field k] (hp2 : 2 ≠ 0) {v s t f₁ w : Polynomial k} (hv_ne : v ≠ 0) (ht_ne : t ≠ 0) (hcop_st : IsCoprime s t) (hcop_ft : IsCoprime f₁ t) (hcurve : v ^ 3 * s ^ 2 * f₁ = t ^ 2 * w) (hv' : Polynomial.derivative v = 0) (hw' : Polynomial.derivative w = 0) : Polynomial.derivative t = 0

Auxiliary step toward Lemma 5.3: from the curve equation v³ · s² · f₁ = t² · w together with v' = w' = 0, deduce that the y-denominator t has zero derivative. This goes through the Wronskian vanishing and then Polynomial.derivative_eq_zero_of_sq.

theorem lemma_5_3 {k : Type u_1} [Field k] {p : ℕ} [CharP k p] (hp : p ≠ 0) (hp2 : 2 ≠ 0) {u v s t f₁ w : Polynomial k} (hcop_uv : IsCoprime u v) (hcop_st : IsCoprime s t) (hcop_ft : IsCoprime f₁ t) (hv_ne : v ≠ 0) (ht_ne : t ≠ 0) (hs_ne : s ≠ 0) (hf₁_sep : f₁.Separable) (hinsep : Polynomial.derivative u * v - u * Polynomial.derivative v = 0) (hcurve : v ^ 3 * s ^ 2 * f₁ = t ^ 2 * w) (hw' : Polynomial.derivative w = 0) : (∃ (f : Polynomial k) (g : Polynomial k), (Polynomial.expand k p) f = u ∧ (Polynomial.expand k p) g = v) ∧ (∃ (t₀ : Polynomial k), (Polynomial.expand k p) t₀ = t) ∧ ∃ (g₂ : Polynomial k), s ^ 2 * f₁ = (Polynomial.expand k p) g₂ ^ 2 * f₁ ^ p

Lemma 5.3 (Sutherland, Section 5.1): let α : E₁ → E₂ be an inseparable isogeny of elliptic curves E₁: y² = f₁(x), E₂: y² = f₂(x) over a field k of characteristic p > 0, written in standard form with u/v for the x-coordinate and s/t · y for the y-coordinate. Then u, v, t are all p-th powers and s² · f₁ factors as (p-th power)² · f₁^p, so the inseparable isogeny factors through Frobenius as α = (a(x^p), b(x^p)·y^p).