baseChange_addX — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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