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