baseChange_equation — Mathlib

English

The polynomial Y after base change B equals the Y-polynomial after base change A mapped via f.

Русский

Полином Y после базового переноса по B равен полиному Y после переноса по A, отображённому через f.

LaTeX

$$$(W.baseChange B).toAffine.polynomialY = (W.baseChange A).toAffine.polynomialY.map (mapRingHom f)$$$

Lean4

theorem baseChange_equation (hf : Function.Injective f) :
    (W.baseChange B).toAffine.Equation (f x) (f y) ↔ (W.baseChange A).toAffine.Equation x y := by
  rw [← map_equation _ _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]

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