English
A constructor that builds an ideal sheaf data from a family of ideals I(U), a basic open compatibility, a support set, and a compatibility with zero loci.
Русский
Конструктор строит данные идеального слоя из семейства идеалов I(U), совместимости c открытыми базисами, поддержки и совместимости с нулевыми локусами.
LaTeX
$$mkOfMemSupportIff(ideal, map_ideal_basicOpen, supportSet, supportSet_inter) gives X.IdealSheafData$$
Lean4
/-- A useful constructor of `IdealSheafData`
with the condition on `supportSet` being easier to check. -/
@[simps ideal coe_support]
def mkOfMemSupportIff (ideal : ∀ U : X.affineOpens, Ideal Γ(X, U))
(map_ideal_basicOpen :
∀ (U : X.affineOpens) (f : Γ(X, U)),
(ideal U).map (X.presheaf.map (homOfLE <| X.basicOpen_le f).op).hom = ideal (X.affineBasicOpen f))
(supportSet : Set X)
(supportSet_inter : ∀ U : X.affineOpens, ∀ x ∈ U.1, x ∈ supportSet ↔ x ∈ X.zeroLocus (U := U.1) (ideal U)) :
X.IdealSheafData where
ideal := ideal
map_ideal_basicOpen := map_ideal_basicOpen
supportSet := supportSet
supportSet_eq_iInter_zeroLocus :=
by
let I' : X.IdealSheafData := { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen }
change supportSet = I'.supportSet
ext x
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
exact (supportSet_inter ⟨U, hU⟩ x hxU).trans (I'.mem_support_iff_of_mem (U := ⟨U, hU⟩) hxU).symm
