map_toSpecMvPoly — Mathlib

English

For any morphism f, the composition map n f with toSpecMvPoly n T equals toSpecMvPoly n S; i.e., the canonical map to the polynomial-motivated spectrum commutes with the base map.

Русский

Для любого f композиция map n f с toSpecMvPoly n T равна toSpecMvPoly n S; каноническое отображение к спектру полиномов сохраняется под основанной карты.

LaTeX

$$$map\\ n\\ f \\circ toSpecMvPoly\\ n\\ T = toSpecMvPoly\\ n\\ S.$$$

Lean4

@[reassoc (attr := simp)]
theorem map_toSpecMvPoly {S T : Scheme.{max u v}} (f : S ⟶ T) : map n f ≫ toSpecMvPoly n T = toSpecMvPoly n S :=
  by
  apply (toSpecMvPolyIntEquiv _).injective
  ext i
  rw [toSpecMvPolyIntEquiv_comp, ← coord, map_appTop_coord, coord]

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