Monoidal composition coherence of quasicoherent pullback

The canonical comparison between successive pullbacks of quasicoherent sheaves and pullback along the composite scheme morphism respects the strong symmetric monoidal structures. Consequently, composing changes of base is compatible with tensor products and structure sheaves, without flatness or finiteness assumptions.

The unit and tensor coherence rules simplify before the generic comp_η and comp_δ equations expand the composite functor and erase the expression these rules match.

The compatibility restricts Scheme.Modules.pullback_comp_δ and Scheme.Modules.pullbackObjUnitIso_comp to quasicoherent sheaves. Mathlib's CategoryTheory.NatTrans.IsMonoidal then supplies compatibility for the inverse comparison.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_comp_η {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.Functor.OplaxMonoidal.η ((pullback g).comp (pullback f)) = CategoryTheory.CategoryStruct.comp ((pullbackComp f g).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (QuasicoherentSheaf Z))) (CategoryTheory.Functor.OplaxMonoidal.η (pullback (CategoryTheory.CategoryStruct.comp f g)))

The inverse unit comparisons of successive pullbacks agree with the comparison for the composite morphism through the canonical composition isomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_comp_η_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : QuasicoherentSheaf X} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit (QuasicoherentSheaf X) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η ((pullback g).comp (pullback f))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((pullbackComp f g).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (QuasicoherentSheaf Z))) (CategoryTheory.Functor.OplaxMonoidal.η (pullback (CategoryTheory.CategoryStruct.comp f g)))) h

The inverse unit comparisons of successive pullbacks agree with the comparison for the composite morphism through the canonical composition isomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_comp_δ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E F : QuasicoherentSheaf Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ ((pullback g).comp (pullback f)) E F) (CategoryTheory.MonoidalCategoryStruct.tensorHom ((pullbackComp f g).hom.app E) ((pullbackComp f g).hom.app F)) = CategoryTheory.CategoryStruct.comp ((pullbackComp f g).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj E F)) (CategoryTheory.Functor.OplaxMonoidal.δ (pullback (CategoryTheory.CategoryStruct.comp f g)) E F)

The inverse tensor comparisons of successive pullbacks agree with the comparison for the composite morphism through the canonical composition isomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_comp_δ_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E F : QuasicoherentSheaf Z) {Z✝ : QuasicoherentSheaf X} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((pullback (CategoryTheory.CategoryStruct.comp f g)).obj E) ((pullback (CategoryTheory.CategoryStruct.comp f g)).obj F) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ ((pullback g).comp (pullback f)) E F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((pullbackComp f g).hom.app E) ((pullbackComp f g).hom.app F)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((pullbackComp f g).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj E F)) (CategoryTheory.Functor.OplaxMonoidal.δ (pullback (CategoryTheory.CategoryStruct.comp f g)) E F)) h

The inverse tensor comparisons of successive pullbacks agree with the comparison for the composite morphism through the canonical composition isomorphism.

instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.isMonoidal_pullbackComp_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.NatTrans.IsMonoidal (pullbackComp f g).hom

The canonical composition isomorphism of quasicoherent pullback is monoidal.