English
The square of the coordinate associated to ψ₂ on the Weierstrass curve equals the coordinate corresponding to Ψ₂Sq, up to a linear term.
Русский
Квадрат координаты ψ₂ на кривой Вейерштрасса равен координате Ψ₂Sq с добавлением линейного слагаемого.
LaTeX
$$$$mk(W,W.\psi_2)^2 = mk(W, C(W.\Psi_2^\, Sq)).$$$$
Lean4
theorem XYIdeal_neg_mul {x y : F} (h : W.Nonsingular x y) :
XYIdeal W x (C <| W.negY x y) * XYIdeal W x (C y) = XIdeal W x :=
by
have Y_rw :
(Y - C (C y)) * (Y - C (C <| W.negY x y)) -
C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
W.polynomial * 1 :=
by
linear_combination (norm := (rw [negY, polynomial]; C_simp; ring1))
congr_arg C (congr_arg C ((equation_iff ..).mp h.left).symm)
simp_rw [XYIdeal, XClass, YClass, span_pair_mul_span_pair, mul_comm, ← map_mul, AdjoinRoot.mk_eq_mk.mpr ⟨1, Y_rw⟩,
map_mul, span_insert, ← span_singleton_mul_span_singleton, ← Ideal.mul_sup, ← span_insert]
convert mul_top (_ : Ideal W.CoordinateRing) using 2
simp_rw [← Set.image_singleton (f := mk W), ← Set.image_insert_eq, ← map_span]
convert map_top (R := F[X][Y]) (mk W) using 1
apply congr_arg
simp_rw [eq_top_iff_one, mem_span_insert', mem_span_singleton']
rcases ((nonsingular_iff' ..).mp h).right with hx | hy
· let W_X := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
refine ⟨C <| C W_X⁻¹ * -(X + C (2 * x + W.a₂)), C <| C <| W_X⁻¹ * W.a₁, 0, C <| C <| W_X⁻¹ * -1, ?_⟩
rw [← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hx]
simp only [W_X, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hx]
C_simp
ring1
· let W_Y := 2 * y + W.a₁ * x + W.a₃
refine ⟨0, C <| C W_Y⁻¹, C <| C <| W_Y⁻¹ * -1, 0, ?_⟩
rw [negY, ← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hy]
simp only [W_Y, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hy]
C_simp
ring1
