Pullback of quasicoherent sheaves preserves duals

Pullback from quasicoherent sheaves to all modules on the source of an arbitrary scheme morphism is strong symmetric monoidal. Its inverse tensor comparison is the canonical oplax tensorator of module pullback, and its inverse unit comparison is the structure-sheaf identification. The existing identity and composition formulas for these canonical comparisons therefore still apply. The canonical QuasicoherentSheaf.pullback functor inherits this strong symmetric monoidal structure, with characteristic equations for all four comparisons on underlying modules. No flatness or finiteness assumptions are needed.

In particular, arbitrary pullback preserves both left and right dualizability inside the quasicoherent subcategories. This lets dualizability be transported to affine charts, where it is equivalent to finite projectivity of the module of global sections.

The monoidal structure is obtained from the invertibility of the existing oplax comparisons, using Mathlib's Functor.Monoidal.ofOplaxMonoidal. Dual preservation then follows from Functor.mapHasLeftDual and Functor.mapHasRightDual.

References

• The Stacks Project, Sheaves of Modules, Lemma 03EL (pullback of tensor products).

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackTensorLeftIso {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] : (CategoryTheory.MonoidalCategory.tensorLeft M).comp (pullback f) ≅ (pullback f).comp (CategoryTheory.MonoidalCategory.tensorLeft ((pullback f).obj M))

Pulling back a tensor product with a fixed quasicoherent left factor commutes with tensoring by its pullback, naturally in the other, arbitrary sheaf of modules.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackTensorLeftIso_hom_app {X Y : Scheme} (f : X ⟶ Y) (M N : Y.Modules) [SheafOfModules.IsQuasicoherent M] : (pullbackTensorLeftIso f M).hom.app N = CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N

The left tensor comparison is the canonical oplax tensor map of pullback.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackTensorRightIso {X Y : Scheme} (f : X ⟶ Y) (N : Y.Modules) [SheafOfModules.IsQuasicoherent N] : (CategoryTheory.MonoidalCategory.tensorRight N).comp (pullback f) ≅ (pullback f).comp (CategoryTheory.MonoidalCategory.tensorRight ((pullback f).obj N))

Pulling back a tensor product with a fixed quasicoherent right factor commutes with tensoring by its pullback, naturally in the other, arbitrary sheaf of modules.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackTensorRightIso_hom_app {X Y : Scheme} (f : X ⟶ Y) (M N : Y.Modules) [SheafOfModules.IsQuasicoherent N] : (pullbackTensorRightIso f N).hom.app M = CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N

The right tensor comparison is the canonical oplax tensor map of pullback.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.pullbackToModulesMonoidal {X Y : Scheme} (f : X ⟶ Y) : ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (pullback f)).Monoidal

Pullback from quasicoherent sheaves to all modules on the source is strong monoidal, with inverse comparisons inherited from module pullback.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackToModules_δ {X Y : Scheme} (f : X ⟶ Y) (E F : TauCeti.AlgebraicGeometry.QuasicoherentSheaf Y) : CategoryTheory.Functor.OplaxMonoidal.δ ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (pullback f)) E F = CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) E.obj F.obj

The inverse tensor comparison is the canonical module-pullback tensor comparison.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackToModules_η {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.Functor.OplaxMonoidal.η ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (pullback f)) = (pullbackObjUnitIso f).hom

The inverse unit comparison is the canonical structure-sheaf identification.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackToModules_μ {X Y : Scheme} (f : X ⟶ Y) (E F : TauCeti.AlgebraicGeometry.QuasicoherentSheaf Y) : CategoryTheory.Functor.LaxMonoidal.μ ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (pullback f)) E F = CategoryTheory.inv (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) E.obj F.obj)

The tensor comparison inverts the canonical module-pullback tensor comparison.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackToModules_ε {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.Functor.LaxMonoidal.ε ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (pullback f)) = (pullbackObjUnitIso f).inv

The unit comparison inverts the canonical structure-sheaf identification.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.pullbackToModulesBraided {X Y : Scheme} (f : X ⟶ Y) : ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (pullback f)).Braided

Pullback of quasicoherent sheaves, viewed in all modules, respects symmetry.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullbackBraided {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : (pullback f).Braided

Pullback of quasicoherent sheaves is strong symmetric monoidal for every scheme morphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_δ_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E F : QuasicoherentSheaf Y) : (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) E F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (AlgebraicGeometry.Scheme.Modules.pullback f) E.obj F.obj) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)))

The inverse tensor comparison of quasicoherent pullback is the module comparison, transported along the underlying-object identifications.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_η_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : (CategoryTheory.Functor.OplaxMonoidal.η (pullback f)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso f).hom

The inverse unit comparison of quasicoherent pullback is the structure-sheaf comparison.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_μ_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E F : QuasicoherentSheaf Y) : (CategoryTheory.Functor.LaxMonoidal.μ (pullback f) E F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Functor.OplaxMonoidal.δ ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (AlgebraicGeometry.Scheme.Modules.pullback f)) E F)) (CategoryTheory.eqToHom ⋯))

The tensor comparison of quasicoherent pullback inverts the module comparison, transported along the underlying-object identifications.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_ε_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : (CategoryTheory.Functor.LaxMonoidal.ε (pullback f)).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso f).inv (CategoryTheory.eqToHom ⋯)

The unit comparison of quasicoherent pullback inverts the structure-sheaf comparison.

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_pullback {X Y : AlgebraicGeometry.Scheme} (E : QuasicoherentSheaf Y) (f : X ⟶ Y) (hE : Nonempty (CategoryTheory.HasLeftDual E)) : Nonempty (CategoryTheory.HasLeftDual ((pullback f).obj E))

Arbitrary pullback carries a left dual of a quasicoherent sheaf to a left dual of its pullback.

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasRightDual_pullback {X Y : AlgebraicGeometry.Scheme} (E : QuasicoherentSheaf Y) (f : X ⟶ Y) (hE : Nonempty (CategoryTheory.HasRightDual E)) : Nonempty (CategoryTheory.HasRightDual ((pullback f).obj E))

Arbitrary pullback preserves right dualizability of quasicoherent sheaves.