English
Let R, S, A, B be commutative rings, W' a Weierstrass affine curve over R, and f : R →+* S a ring homomorphism. For any x1, x2, ℓ ∈ A, the X-coordinate operation is compatible with base change along f: applying addX after base-changing to B and then mapping inputs via f is the same as mapping the original addX to A via f.
Русский
Пусть R, S, A, B - коммутативные кольца, W' - аффинная кривая Вейерштрасса над R, и f: R →+* S - кольцевой гомоморфизм. Для любых x1, x2, ℓ ∈ A операция X-координаты совместима с базовым изменением по f: применение addX после изменения основания к B и последующее отображение входов через f равносильно отображению исходного addX в A через f.
LaTeX
$$$ (W'.baseChange B).toAffine.addX (f x_1) (f x_2) (f \ell) = f \bigl((W'.baseChange A).toAffine.addX x_1 x_2 \ell\bigr) $$$
Lean4
theorem baseChange_addX :
(W'.baseChange B).toAffine.addX (f x₁) (f x₂) (f ℓ) = f ((W'.baseChange A).toAffine.addX x₁ x₂ ℓ) := by
rw [← RingHom.coe_coe, ← map_addX, map_baseChange]
