English
Let W be a Weierstrass curve over a commutative ring R, and suppose S is an R-algebra and A, B are algebras with a scalar-tower structure as in the statement. For an algebra hom f: A →_S B, the ψ₂ polynomial of the base-changed curve over B is the image, under the induced map, of the ψ₂ polynomial of the base-changed curve over A.
Русский
Пусть W — кривая Вейерштрасса над коммутативным кольцом R, S — R-алгебра, A и B — алгебры с тензорной (scalartower) структурой над R, и f: A →_S B — алгебра-гомоморфизм. Тогда полином ψ₂ базового изменения кривой над B равен образу полинома ψ₂ базового изменения над A под индуцированным отображением.
LaTeX
$$$ (W.baseChange\ B).\psi_2 = (W.baseChange\ A).\psi_2.map (\text{mapRingHom } f) $$$
Lean4
theorem baseChange_ψ₂ : (W.baseChange B).ψ₂ = (W.baseChange A).ψ₂.map (mapRingHom f) := by rw [← map_ψ₂, map_baseChange]
