English
Let W be an affine Weierstrass curve over a commutative ring R, and let f be a ring homomorphism R →+* S. If a pair (x, y) satisfies the equation of W, then the pair (f x, f y) satisfies the equation of the base-changed curve W.map f over S; i.e., the defining polynomial of W maps to the defining equation of the image under f.
Русский
Пусть W — аффинная кривая Вейерштрасса над кольцом R, а f — гомоморфизм колец R →+* S. Если пара (x, y) удовлетворяет уравнению W, то пара (f x, f y) удовлетворяет уравнению кривой, полученной после базового переноса W.map f над S; то есть образующая полином определяющего уравнения кривой отображается под f в уравнение изображения.
LaTeX
$$$P_W(x,y)=0 \Rightarrow P_W^{f}(f x, f y)=0$$$
Lean4
theorem map {x y : R} (h : W.Equation x y) : (W.map f).toAffine.Equation (f x) (f y) := by
rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]
