map — Mathlib

English

If P lies on the Weierstrass projective curve, then after applying a ring homomorphism f, the image curve has equation obtained by mapping P via f to the target ring.

Русский

Если P лежит на проективной кривой Вейерштрасса, то после отображения через гомоморфизм f получаемое изображение имеет уравнение, полученное отображением P через f в целевое кольцо.

LaTeX

$$$h:\\ W'.Equation P \\Rightarrow (W'.map f).toProjective.Equation (f \\circ P)$$$

Lean4

theorem map (h : W'.Equation P) : (W'.map f).toProjective.Equation (f ∘ P) := by
  rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]

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