Identity coherence for tensor products under scheme-module pullback

Mathlib's Scheme.Modules.pullbackId identifies pullback along the identity scheme morphism with the identity functor. The tensor comparison commutes with this identification on both factors. Together with Scheme.Modules.pullbackObjUnitIso_id for the unit and Scheme.Modules.pullback_comp_δ for composition, this gives the identity and composition normalizations of the canonical oplax monoidal pullback structure.

The result specializes the identity coherence for sheaves of modules on a ringed site, with no finiteness or quasi-coherence assumptions on the modules.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullback_id_δ (X : Scheme) (M N : X.Modules) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (pullback (CategoryTheory.CategoryStruct.id X)) M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom ((pullbackId X).hom.app M) ((pullbackId X).hom.app N)) = (pullbackId X).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)

The canonical tensor comparison for pullback along the identity scheme morphism respects Mathlib's identity isomorphism of module pullback.

@[simp]

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

The canonical tensor comparison for pullback along the identity scheme morphism respects Mathlib's identity isomorphism of module pullback.