baseChange_addY — Mathlib

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]

Похожие утверждения