support_map — Mathlib

English

In the special case of a quasi-compact morphism, the pushforward of the vanishing ideal along f equals the vanishing ideal of the closure of the image of the closed set Z.

Русский

Для квазимонтонного морфизма f образ переноса идеала исчезновения совпадает с идеалом исчезновения замыкания образа замкнутого множества.

LaTeX

$$$ (\\vanishingIdeal Z).map f = \\vanishingIdeal(\\overline{f(Z)}) $$$

Lean4

@[simp]
theorem support_map (I : X.IdealSheafData) (f : X ⟶ Y) [QuasiCompact f] :
    (I.map f).support = .closure (f.base '' I.support) :=
  by
  ext1
  rw [map, Scheme.Hom.support_ker, Scheme.comp_base, TopCat.coe_comp, Set.range_comp, range_subschemeι,
    TopologicalSpace.Closeds.coe_closure]

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