Pullback of an ideal sheaf as a sheaf of modules

Let g : X ⟶ Y be a morphism of schemes and I ⊆ 𝒪_Y an ideal sheaf. There are two ways to pull I back to X: the inverse image I.comap g, the ideal sheaf of the fibre product X ×_Y V(I), and the pullback g^* I of I as an 𝒪_Y-module. Pulling back the inclusion I ⟶ 𝒪_Y gives g^* I ⟶ g^* 𝒪_Y ≅ 𝒪_X, whose image is generated by the functions g^♯ s for sections s of I; these lie in I.comap g (app_mem_sections_comap). So the composite factors through I.comap g ⊆ 𝒪_X, giving the comparison morphism g^* I ⟶ I.comap g.

The comparison is not an isomorphism in general: for the inclusion g of V(I), the pullback g^* I is I / I² while I.comap g is zero. It is one for effective Cartier divisors whose inverse image is again effective Cartier (Scheme.IdealSheafData.isIso_pullbackSheafHom in TauCeti.AlgebraicGeometry.EffectiveCartierDivisor.Pullback).

Main declarations

• Scheme.IdealSheafData.app_mem_sections_comap: g^♯ carries sections of I to sections of I.comap g;
• Scheme.IdealSheafData.pullbackSheafHom: the comparison morphism g^* I ⟶ I.comap g, characterized by pullbackSheafHom_sheafι, and computed on the images of sections of I under the unit of the pullback–pushforward adjunction by pullbackSheafHom_app_unit_app.

References

• The Stacks Project, Divisors, Section Effective Cartier divisors (Tag 01WQ), where the pullback of an effective Cartier divisor is defined.

theorem AlgebraicGeometry.Scheme.IdealSheafData.app_mem_sections_comap {X Y : Scheme} (I : Y.IdealSheafData) (g : X ⟶ Y) {U : Y.Opens} {s : ↑(Y.presheaf.obj (Opposite.op U))} (hs : s ∈ I.sections U) : (CategoryTheory.ConcreteCategory.hom (Hom.app g U)) s ∈ (I.comap g).sections ((TopologicalSpace.Opens.map g.base).obj U)

Pulling back along g carries sections of I to sections of the inverse image of I.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.pullbackSheafHom {X Y : Scheme} (I : Y.IdealSheafData) (g : X ⟶ Y) : (Modules.pullback g).obj I.sheaf ⟶ (I.comap g).sheaf

The canonical morphism g^* I ⟶ I.comap g from the pullback of an ideal sheaf to the ideal sheaf of its inverse image: the pullback g^* I ⟶ g^* 𝒪_Y ≅ 𝒪_X of the inclusion I ⟶ 𝒪_Y factors through I.comap g ⊆ 𝒪_X (pullbackSheafHom_sheafι).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.pullbackSheafHom_sheafι {X Y : Scheme} (I : Y.IdealSheafData) (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (I.pullbackSheafHom g) (I.comap g).sheafι = CategoryTheory.CategoryStruct.comp ((Modules.pullback g).map I.sheafι) (Modules.pullbackObjUnitIso g).hom

The morphism pullbackSheafHom followed by the inclusion I.comap g ⟶ 𝒪_X is the pullback of the inclusion I ⟶ 𝒪_Y.

theorem AlgebraicGeometry.Scheme.IdealSheafData.pullbackSheafHom_sheafι_assoc {X Y : Scheme} (I : Y.IdealSheafData) (g : X ⟶ Y) {Z : X.Modules} (h : SheafOfModules.unit X.ringCatSheaf ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (I.pullbackSheafHom g) (I.comap g).sheafι) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((Modules.pullback g).map I.sheafι) (Modules.pullbackObjUnitIso g).hom) h

The morphism pullbackSheafHom followed by the inclusion I.comap g ⟶ 𝒪_X is the pullback of the inclusion I ⟶ 𝒪_Y.

theorem AlgebraicGeometry.Scheme.IdealSheafData.pullbackSheafHom_app_unit_app {X Y : Scheme} (I : Y.IdealSheafData) (g : X ⟶ Y) (U : Y.Opens) (t : ↑(I.sheaf.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app (I.pullbackSheafHom g) ((TopologicalSpace.Opens.map g.base).obj U))) ((CategoryTheory.ConcreteCategory.hom (Modules.Hom.app ((Modules.pullbackPushforwardAdjunction g).unit.app I.sheaf) U)) t) = (I.comap g).sectionMk ((CategoryTheory.ConcreteCategory.hom (Hom.app g U)) ((CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι U)) t)) ⋯

The morphism pullbackSheafHom sends the image of a section t of I under the unit of the adjunction to the section g^♯ t of I.comap g.