Ideal sheaves generated by global sections

For a scheme X and an ideal I of its ring of global sections, Mathlib's AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop I is the quasi-coherent ideal sheaf I·𝒪_X generated by I. This file records how these ideal sheaves interact with morphisms of schemes.

Main results

• AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_le_ker_iff: I·𝒪_Y is contained in the kernel of f : X ⟶ Y exactly when f^* kills I, that is, when f factors through the zero scheme of I; AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_le_ker_comp_iff transports this condition along a composite g ≫ f, replacing I by f^*(I);
• AlgebraicGeometry.Scheme.Hom.ker_Spec_map: the kernel of Spec S ⟶ Spec R is the ideal sheaf of the kernel of the ring map;
• AlgebraicGeometry.Scheme.IdealSheafData.comap_ofIdealTop: the inverse image ideal sheaf of I·𝒪_Y along f : X ⟶ Y is f^*(I)·𝒪_X, so the zero scheme of I pulls back to the zero scheme of f^*(I);
• AlgebraicGeometry.Scheme.Hom.ker_pullback_fst_Spec_map: the base change of the closed immersion Spec S ⟶ Spec R along f : X ⟶ Spec R is the zero scheme of the ideal of 𝒪_X generated by the pullback of the kernel of R → S.

The last statement is the scheme-theoretic form of the identity X ×_{Spec R} Spec (R ⧸ I) = V(I·𝒪_X), for instance for the fibres of a scheme over a local ring.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_le_ker_iff {X Y : Scheme} (f : X ⟶ Y) (I : Ideal ↑(Y.presheaf.obj (Opposite.op ⊤))) : ofIdealTop I ≤ Hom.ker f ↔ I ≤ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f))

The ideal sheaf generated by an ideal I of global sections of Y is contained in the kernel of f : X ⟶ Y exactly when the pullback of every element of I vanishes on X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_le_ker_comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Z ⟶ X) (I : Ideal ↑(Y.presheaf.obj (Opposite.op ⊤))) : ofIdealTop I ≤ Hom.ker (CategoryTheory.CategoryStruct.comp g f) ↔ ofIdealTop (Ideal.map (CommRingCat.Hom.hom (Hom.appTop f)) I) ≤ Hom.ker g

The ideal sheaf generated by an ideal I of global sections of Y is contained in the kernel of a composite g ≫ f with f : X ⟶ Y exactly when the ideal sheaf generated by the pullback f^*(I) is contained in the kernel of g.

theorem AlgebraicGeometry.Scheme.Hom.ker_Spec_map {R S : CommRingCat} (φ : R ⟶ S) : ker (Spec.map φ) = IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (ΓSpecIso R).inv) (RingHom.ker (CommRingCat.Hom.hom φ)))

The kernel of the morphism Spec S ⟶ Spec R induced by a ring map R ⟶ S is the ideal sheaf of the kernel of the ring map, read in the global sections of Spec R.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_ofIdealTop {X Y : Scheme} (I : Ideal ↑(Y.presheaf.obj (Opposite.op ⊤))) (f : X ⟶ Y) : (ofIdealTop I).comap f = ofIdealTop (Ideal.map (CommRingCat.Hom.hom (Hom.appTop f)) I)

Inverse image of the ideal sheaf generated by global sections. The inverse image along f : X ⟶ Y of the ideal sheaf generated by an ideal I of global sections of Y is the ideal sheaf generated by the pullbacks of the elements of I: the zero scheme of I pulls back to the zero scheme of f^*(I).

theorem AlgebraicGeometry.Scheme.Hom.ker_pullback_fst_Spec_map {X : Scheme} {R S : CommRingCat} (φ : R ⟶ S) [IsClosedImmersion (Spec.map φ)] (f : X ⟶ Spec R) : ker (CategoryTheory.Limits.pullback.fst f (Spec.map φ)) = IdealSheafData.ofIdealTop (Ideal.map ((CommRingCat.Hom.hom (appTop f)).comp (CommRingCat.Hom.hom (ΓSpecIso R).inv)) (RingHom.ker (CommRingCat.Hom.hom φ)))

Base change of a closed subscheme of an affine scheme. For a ring map R ⟶ S whose induced morphism Spec S ⟶ Spec R is a closed immersion, for instance a surjective ring map, the base change of this closed immersion along f : X ⟶ Spec R is the zero scheme of the ideal of 𝒪_X generated by the pullback of the kernel of R ⟶ S.