English
Let f be as above. The AddY operation is compatible with base change: base-changing W' to B and mapping inputs via f yields the same as mapping the original AddY over A via f.
Русский
Пусть f как выше. Операция AddY совместима с базовым изменением: смена основания W' на B с отображением входов через f дает тот же результат, что отображение исходного AddY с A через f.
LaTeX
$$$ (W'.baseChange B).toAffine.addY (f x_1) (f x_2) (f y_1) (f \ell) = f ((W'.baseChange A).toAffine.addY x_1 x_2 y_1 \ell) $$$
Lean4
theorem baseChange_addY :
(W'.baseChange B).toAffine.addY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((W'.baseChange A).toAffine.addY x₁ x₂ y₁ ℓ) := by
rw [← RingHom.coe_coe, ← map_addY, map_baseChange]