baseChange_Ψ₃ — Mathlib

English

Under the same setup, the degree-3 division polynomial Ψ₃ behaves well with base change: the Ψ₃ polynomial of the base-changed curve over B is the image under the induced map of the Ψ₃ polynomial of the base-changed curve over A.

Русский

В том же контексте полином Ψ₃, соответствующий кривой базисного изменения, корректно переносится через отображение: Ψ₃ базового изменения над B равен образу Ψ₃ над A.

LaTeX

$$$ (W.baseChange\ B).\\Psi_3 = (W.baseChange\ A).\\Psi_3.map f $$$

Lean4

theorem baseChange_Ψ₃ : (W.baseChange B).Ψ₃ = (W.baseChange A).Ψ₃.map f := by rw [← map_Ψ₃, map_baseChange]

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