baseChange_equation — Mathlib

English

Under base change, the X-coordinate polynomial maps compatibly with the base-changed curve.

Русский

При изменении базы координатная полиномная X соответствует базовому изменению кривой.

LaTeX

$$$(W'.baseChange B).toProjective.polynomialX = MvPolynomial.map f (W'.baseChange A).toProjective.polynomialX$$$

Lean4

theorem baseChange_equation (hf : Function.Injective f) :
    (W'.baseChange B).toProjective.Equation (f ∘ P) ↔ (W'.baseChange A).toProjective.Equation P := by
  rw [← RingHom.coe_coe, ← map_equation P hf, AlgHom.toRingHom_eq_coe, map_baseChange]

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