baseChange_addXYZ — Mathlib

English

Let W′ be a Weierstrass projective curve over R. For P, Q : Fin 3 → A and f : A →ₛ B, the negAddY operator is compatible with base change:

Русский

Пусть W′ — проектная кривая Вейерштрасса над R. Для P, Q : Fin 3 → A и f : A →ₛ B операция negAddY сохраняется при базовом изменении:

LaTeX

$$$$(W'.baseChange B).toProjective.negAddY (f \circ P) (f \circ Q) = f \bigl((W'.baseChange A).toProjective.negAddY P Q\bigr)$$$$

Lean4

theorem baseChange_addXYZ :
    (W'.baseChange B).toProjective.addXYZ (f ∘ P) (f ∘ Q) = f ∘ (W'.baseChange A).toProjective.addXYZ P Q := by
  rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]

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