baseChange_negAddY — Mathlib

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]

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