English
Let X be a scheme and I an ideal sheaf data on X. For every closed subset Z of X, Z is contained in the support of I if and only if I is contained in the vanishing ideal of Z.
Русский
Пусть X — схема, I — данные идеала-однородного пучка на X. Для любой замкнутой группы Z в X справедливо: Z ⊆ Supp(I) тогда и только если I ⊆ vanishingIdeal(Z).
LaTeX
$$$Z \\subseteq \\mathrm{Supp}(I) \\iff I \\subseteq \\operatorname{vanishingIdeal}(Z)$$$
Lean4
theorem le_support_iff_le_vanishingIdeal {I : X.IdealSheafData} {Z : Closeds X} :
Z ≤ I.support ↔ I ≤ vanishingIdeal Z :=
by
simp only [le_def, vanishingIdeal_ideal, ← PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal]
trans ∀ U : X.affineOpens, (Z : Set X) ∩ U ⊆ I.support ∩ U
· refine ⟨fun H U x hx ↦ ⟨H hx.1, hx.2⟩, fun H x hx ↦ ?_⟩
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
exact (H ⟨U, hU⟩ ⟨hx, hxU⟩).1
refine forall_congr' fun U ↦ ?_
rw [coe_support_inter, ← Set.image_subset_image_iff U.2.fromSpec.isOpenEmbedding.injective,
Set.image_preimage_eq_inter_range, IsAffineOpen.fromSpec_image_zeroLocus, IsAffineOpen.range_fromSpec]
