English
Let I be an ideal sheaf data on a scheme X and U an affine open. Then the intersection of the zero locus of I on U with U is contained in the support of I.
Русский
Пусть I — данные идеального слоя на схеме X, и пусть U — аффинное открытое. Тогда пересечение нулевой локусы I на U с U содержится в поддержке I.
LaTeX
$$$X\!:\!zeroLocus(I(I).ideal(U)) \cap U \subseteq I.supportSet$$$
Lean4
theorem zeroLocus_inter_subset_supportSet (I : IdealSheafData X) (U : X.affineOpens) :
X.zeroLocus (U := U.1) (I.ideal U) ∩ U ⊆ I.supportSet :=
by
rw [I.supportSet_eq_iInter_zeroLocus]
refine Set.subset_iInter fun V ↦ ?_
apply (X.codisjoint_zeroLocus (U := V) (I.ideal V)).symm.left_le_of_le_inf_right
rintro x ⟨⟨hx, hxU⟩, hxV⟩
simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe] at hx ⊢
intro s hfU hxs
obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, hxV⟩
have inst := U.2.isLocalization_basicOpen f
have := (I.map_ideal (U := X.affineBasicOpen f) (hfg.trans_le (X.basicOpen_le g))).le (Ideal.mem_map_of_mem _ hfU)
rw [← I.map_ideal_basicOpen] at this
obtain ⟨⟨s', ⟨_, n, rfl⟩⟩, hs'⟩ := (IsLocalization.mem_map_algebraMap_iff (.powers f) Γ(X, X.basicOpen f)).mp this
apply_fun (x ∈ X.basicOpen ·) at hs'
refine hx s' s'.2 ?_
cases n <;> simpa [RingHom.algebraMap_toAlgebra, ← hfg, hxf, hxs, Scheme.basicOpen_pow] using hs'
