Monoidal identity coherence of quasicoherent pullback

The canonical isomorphism from pullback along the identity scheme morphism to the identity functor on quasicoherent sheaves respects the strong symmetric monoidal structures. Identifying identity pullback with the original sheaf therefore also identifies the tensor and unit comparisons. This is the identity normalization needed to transport tensor products and duality across changes of base.

The isomorphism is the existing module-pullback identity comparison, restricted to quasicoherent sheaves. Its compatibility is inherited from the tensor and structure-sheaf equations for module pullback, with no flatness or finiteness hypothesis.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_id_η (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor.OplaxMonoidal.η (pullback (CategoryTheory.CategoryStruct.id X)) = (pullbackId X).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (QuasicoherentSheaf X))

The inverse unit comparison of identity pullback is its canonical identity isomorphism at the structure sheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_id_δ (X : AlgebraicGeometry.Scheme) (E F : QuasicoherentSheaf X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (pullback (CategoryTheory.CategoryStruct.id X)) E F) (CategoryTheory.MonoidalCategoryStruct.tensorHom ((pullbackId X).hom.app E) ((pullbackId X).hom.app F)) = (pullbackId X).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj E F)

The inverse tensor comparison of identity pullback is compatible with the canonical identification with the identity functor.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_id_δ_assoc (X : AlgebraicGeometry.Scheme) (E F : QuasicoherentSheaf X) {Z : QuasicoherentSheaf X} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj E F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (pullback (CategoryTheory.CategoryStruct.id X)) E F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((pullbackId X).hom.app E) ((pullbackId X).hom.app F)) h) = CategoryTheory.CategoryStruct.comp ((pullbackId X).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj E F)) h

The inverse tensor comparison of identity pullback is compatible with the canonical identification with the identity functor.

instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.isMonoidal_pullbackId_hom (X : AlgebraicGeometry.Scheme) : CategoryTheory.NatTrans.IsMonoidal (pullbackId X).hom

The identity isomorphism of quasicoherent pullback is monoidal.