English
Let W' be a Weierstrass projective curve over R and f a ring homomorphism R → S. After base-changing along B and along A, the Y-coordinate polynomial of the base-changed curve corresponds under the induced map to the Y-coordinate polynomial of the other base-change. In particular, the Y-polynomial commutes with base-change.
Русский
Пусть W' — проективная кривая Вейерштрасса над кольцом R, и f: R → S — гомоморфизм колец. При базовом изменении по B и по A координатная Y-полином кривой ведёт себя совместимо с образом по f: polynomialY после базового изменения на B равен образу по MvPolynomial.map f от polynomialY после базового изменения на A.
LaTeX
$$$ (W'.baseChange B).toProjective.polynomialY = \\mathrm{MvPolynomial.map}\\ f\\left((W'.baseChange A).toProjective.polynomialY\\right) $$$
Lean4
theorem baseChange_polynomialY :
(W'.baseChange B).toProjective.polynomialY = MvPolynomial.map f (W'.baseChange A).toProjective.polynomialY := by
rw [← map_polynomialY, map_baseChange]
