English
Let f: X → Y be a morphism of schemes and Z a closed subset of X. The image of the vanishing ideal under f is the vanishing ideal of the closure of f(Z) in Y.
Русский
Пусть f: X → Y — морфизм схем, Z — замкнутая подмножина X. Образ идеала исчезновения под действием f равен идеалу исчезновения замыкания f(Z) в Y.
LaTeX
$$$ (\\vanishingIdeal Z).map f = \\vanishingIdeal(\\overline{f(Z)}) $$$
Lean4
theorem map_vanishingIdeal {X Y : Scheme} (f : X ⟶ Y) (Z : TopologicalSpace.Closeds X) :
(vanishingIdeal Z).map f = vanishingIdeal (.closure (f.base '' Z)) :=
by
apply le_antisymm
· rw [map, ← le_support_iff_le_vanishingIdeal, TopologicalSpace.Closeds.closure_le]
refine .trans ?_ (Hom.range_subset_ker_support _)
rw [Scheme.comp_base, TopCat.coe_comp, Set.range_comp, range_subschemeι, coe_support_vanishingIdeal]
·
simp [le_map_iff_comap_le, ← le_support_iff_le_vanishingIdeal, ← Set.image_subset_iff, subset_closure,
← SetLike.coe_subset_coe]
