Pullback of tensor products from an affine base

For a morphism f : X ⟶ Y with affine target Y, the canonical comparison f^*(M ⊗ N) ⟶ f^*M ⊗ f^*N is an isomorphism whenever either factor is quasicoherent. The other factor is an arbitrary sheaf of modules. No flatness or finiteness assumption is required. The comparison is the tensor map of the existing oplax monoidal pullback, so its associativity and unit compatibilities are retained. These affine statements are the local input for the same comparison over an arbitrary target (Scheme.Modules.isIso_pullback_δ_of_isQuasicoherent in TauCeti.AlgebraicGeometry.Modules.Pullback.Quasicoherent).

In particular, pullback from quasicoherent sheaves on Y to modules on X is strong symmetric monoidal (Scheme.Modules.pullbackFromAffineBraided). The tensor comparisons are also exposed as natural isomorphisms with either quasicoherent factor fixed. These affine computations let tensor and duality constructions on sheaves be compared with their module counterparts. For instance, pullback from Y carries a quasicoherent sheaf with a left or right dual in QuasicoherentSheaf Y to one with the corresponding dual in QuasicoherentSheaf X.

References

• The Stacks Project, Sheaves of Modules, Lemma 03EL (pullback of tensor products).
• R. Hartshorne, Algebraic Geometry, Proposition II.5.2.

theorem AlgebraicGeometry.Scheme.Modules.isIso_pullback_δ_of_isAffine {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (M N : Y.Modules) [SheafOfModules.IsQuasicoherent M] : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N)

Pullback from an affine base preserves a tensor product with a quasicoherent left factor. The right factor need not be quasicoherent.

theorem AlgebraicGeometry.Scheme.Modules.isIso_pullback_δ_right_of_isAffine {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (M N : Y.Modules) [SheafOfModules.IsQuasicoherent N] : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N)

Pullback from an affine base preserves a tensor product with a quasicoherent right factor. The left factor need not be quasicoherent.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackTensorLeftIso {X Y : Scheme} [IsAffine Y] (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 the tensor product with a fixed quasicoherent left factor from an affine scheme commutes with tensoring by its pullback, naturally in the other sheaf.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackTensorLeftIso f M = CategoryTheory.asIso ((AlgebraicGeometry.Scheme.Modules.pullback f).oplaxCommTensorLeft M)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackTensorLeftIso_hom_app {X Y : Scheme} [IsAffine Y] (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} [IsAffine Y] (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 the tensor product with a fixed quasicoherent right factor from an affine scheme commutes with tensoring by its pullback, naturally in the other sheaf.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackTensorRightIso f N = CategoryTheory.asIso ((AlgebraicGeometry.Scheme.Modules.pullback f).oplaxCommTensorRight N)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackTensorRightIso_hom_app {X Y : Scheme} [IsAffine Y] (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.pullbackFromAffineMonoidal {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (pullback f)).Monoidal

Pullback of quasicoherent sheaves from an affine scheme, viewed in the category of all modules on the source, is strong monoidal. Its inverse tensor comparison is the canonical oplax tensor map of module pullback.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackFromAffine_δ {X Y : Scheme} [IsAffine Y] (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 of strong monoidal affine pullback is the canonical tensor comparison of the underlying module pullback.

@[simp]

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

The inverse unit comparison of strong monoidal affine pullback is the canonical identification of the pulled-back structure sheaf.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackFromAffine_map_braiding {X Y : Scheme} (f : X ⟶ Y) (E F : TauCeti.AlgebraicGeometry.QuasicoherentSheaf Y) : ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).ι.comp (pullback f)).map (β_ E F).hom = (pullback f).map (β_ E.obj F.obj).hom

Pullback sends the inherited braiding of quasicoherent sheaves to the pullback of the braiding of their underlying sheaves of modules.

@[instance_reducible]

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

Pullback of quasicoherent sheaves from an affine base to modules on the source is symmetric monoidal, with the existing canonical tensor comparisons.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackFromAffineBraided f = { toMonoidal := AlgebraicGeometry.Scheme.Modules.pullbackFromAffineMonoidal f, braided := ⋯ }

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

Pullback along a morphism to an affine scheme preserves dualizability of quasicoherent sheaves: the pullback of a left dual of E is a left dual of the pullback of E.

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

Pullback along a morphism to an affine scheme preserves right dualizability of quasicoherent sheaves.