baseChange_addY — Mathlib

English

Let W′ be a Weierstrass projective curve over R. For P, Q : Fin 3 → A and f : A →ₛ B, the addXYZ operation respects base change:

Русский

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

LaTeX

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

Lean4

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

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