Affine descriptions of pullback ideal sheaves

Restricting ideal sheaf data to an affine open subscheme U, or pulling it back along Spec Γ(X, U) ⟶ X, gives the ideal sheaf generated by its ideal of sections on that open. This file records both equalities, so local equations can be transported using Mathlib's actual closed subscheme construction.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_ι_eq_ofIdealTop {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.comap (↑U).ι = ofIdealTop (Ideal.map (CommRingCat.Hom.hom (↑U).topIso.inv) (I.ideal U))

Restricting an ideal sheaf to an affine open gives the ideal sheaf generated by its ideal on that open, transported to the global sections of the open subscheme.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_fromSpec_eq_ofIdealTop {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) : I.comap hU.fromSpec = ofIdealTop (Ideal.map (CommRingCat.Hom.hom (ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv) (I.ideal ⟨U, hU⟩))

Pulling an ideal sheaf back along Spec Γ(X, U) ⟶ X for an affine open U gives the ideal sheaf generated by its ideal on U, read in the global sections of Spec Γ(X, U).