Locality of ideal sheaf data

An ideal sheaf is determined by its pullbacks to an open cover. This lets affine computations of ideal sheaves, such as Fitting ideals, be glued on an arbitrary scheme.

theorem AlgebraicGeometry.Scheme.IdealSheafData.iInf_map_comap_openCover {X : Scheme} (I : X.IdealSheafData) (𝒰 : X.OpenCover) : ⨅ (i : 𝒰.I₀), (I.comap (𝒰.f i)).map (𝒰.f i) = I

An ideal sheaf is the intersection of the pushforwards of its restrictions to an open cover.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_of_comap_openCover {X : Scheme} {I J : X.IdealSheafData} (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.I₀), I.comap (𝒰.f i) = J.comap (𝒰.f i)) : I = J

Ideal sheaves with equal pullbacks to every member of an open cover are equal.