Gluing of ideal sheaves along an open cover #

Given an open cover 𝒰 of X and closed subschemes V(I i) ⊆ 𝒰.X i that agree on the overlaps — (I i).comap (pullback.fst) = (I j).comap (pullback.snd) on 𝒰.X i ×_X 𝒰.X j — there is a unique closed subscheme Z ⊆ X with Z ∩ 𝒰.X i = V(I i), i.e. a unique ideal sheaf glue 𝒰 I compat with (glue 𝒰 I compat).comap (𝒰.f i) = I i. This is the gluing of the local centres in Kollár's construction of a blow-up sequence functor from its restrictions to the members of a cover: "the subschemes Z'₀ᵢ ⊂ Uᵢ glue together to a subscheme Z₀ ⊂ X" [Kol07, Proposition 37, proof].

The construction #

Mathlib's IdealSheafData is a family of ideals on the affine opens with a localization compatibility, and for an infinite cover the naive sectionwise construction runs into the non-commutation of infinite intersections with localization; so the closed subscheme is glued as a scheme, by the relative gluing lemma [TSPA, Tag 01LH], and its ideal sheaf is read off as a kernel.

A locally directed refinement of the cover. The index type GlueIdx 𝒰 is the set of pairs p = (i, V) with V an affine open of 𝒰.X i, preordered by the images 𝒰.f i ''ᵁ V ⊆ X. The cover glueCover 𝒰 of X by these images (as the schemes V with V.ι ≫ 𝒰.f i) is locally directed in Mathlib's sense (Scheme.Cover.LocallyDirected): for p ≤ q the open immersion V_p ⟶ V_q over X is the transition map, and two members meeting at a point contain a common affine member around it (the affine basic opens form a basis).
The relative gluing datum. Over p = (i, V) put the closed subscheme Z_p := V((I i).comap V.ι) of V; for p ≤ q the transition map carries Z_p into Z_q because the two ideal sheaves agree there — this is exactly the compatibility hypothesis, transported to V_p through V_p ⟶ 𝒰.X i ×_X 𝒰.X j (comap_transition) — and the square Z_p → Z_q over V_p → V_q is cartesian because a closed subscheme is its ideal sheaf (Mathlib's isPullback_of_isClosedImmersion). This is a RelativeGluingData, so Mathlib glues the Z_p to a scheme glueScheme over X (glueι) whose restriction to each member V_p is Z_p (isPullback_natTrans_ι_toBase).
The ideal sheaf. glueι is a closed immersion because it is one over every member of an open cover (closed immersions are local on the target), and glue 𝒰 I compat := glueι.ker. Its inverse image on 𝒰.X i is I i: on every affine open V ⊆ 𝒰.X i both sides pull back to the kernel of Z_{(i,V)} ⟶ V, which is (I i).comap V.ι (ker_fst_of_isClosedImmersion, ker_subschemeι), and an ideal sheaf is determined by its restrictions to an open cover, itself a consequence of extensionality by stalks (ext_stalkIdeal of Hironaka.Scheme.BlowUp.Descent; the stalk maps of an open immersion are isomorphisms). Uniqueness is the same extensionality.

Nothing is assumed about 𝒰 beyond being an open cover indexed in the universe of X; the members and their overlaps may be non-affine and infinite in number.