Pullback of internal Hom from a quasicoherent sheaf

For a quasicoherent sheaf M and an arbitrary sheaf of modules F on Y, construct the canonical comparison f* 𝓗om(M, F) ⟶ 𝓗om(f* M, f* F) for every scheme morphism f : X ⟶ Y. It is invertible whenever M has a quasicoherent left dual. In particular, this applies to finite locally free sources, without flatness of f or finiteness of the target.

The comparison is the mate of the inverse tensor comparison with left factor M. It is characterized by evaluation, is natural in every target sheaf of modules, and is natural in the quasicoherent source. Use TauCeti.AlgebraicGeometry.pullbackIhomComparison M f for the comparison. Invertibility follows by identifying internal Hom with tensoring by the dual, and using the tensor comparison with that quasicoherent dual as left factor. The proof uses TauCeti.ihomIsoTensorLeft and CategoryTheory.Functor.mapExactPairing to transport an exact pairing through pullback on quasicoherent sheaves.

References

• The Stacks Project, Tag 0C6I (base change for sheaf Hom).

noncomputable def TauCeti.AlgebraicGeometry.pullbackIhomComparison {X Y : AlgebraicGeometry.Scheme} (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] (f : X ⟶ Y) : (CategoryTheory.ihom M).comp (AlgebraicGeometry.Scheme.Modules.pullback f) ⟶ (AlgebraicGeometry.Scheme.Modules.pullback f).comp (CategoryTheory.ihom ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M))

The canonical base-change comparison for internal Hom from a quasicoherent sheaf. It is natural in arbitrary target sheaves of modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.whiskerLeft_pullbackIhomComparison_app_comp_ev {X Y : AlgebraicGeometry.Scheme} (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] (f : X ⟶ Y) (F : Y.Modules) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M) ((pullbackIhomComparison M f).app F)) ((CategoryTheory.ihom.ev ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M)).app ((AlgebraicGeometry.Scheme.Modules.pullback f).obj F)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Functor.OplaxMonoidal.δ (AlgebraicGeometry.Scheme.Modules.pullback f) M (M ⟹ F))) ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((CategoryTheory.ihom.ev M).app F))

Evaluation after the base-change comparison is the pullback of evaluation, preceded by the inverse canonical tensor comparison. This characterizes the base-change map.

@[simp]

theorem TauCeti.AlgebraicGeometry.whiskerLeft_pullbackIhomComparison_app_comp_ev_assoc {X Y : AlgebraicGeometry.Scheme} (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] (f : X ⟶ Y) (F : Y.Modules) {Z : X.Modules} (h : (AlgebraicGeometry.Scheme.Modules.pullback f).obj F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M) ((pullbackIhomComparison M f).app F)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M)).app ((AlgebraicGeometry.Scheme.Modules.pullback f).obj F)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Functor.OplaxMonoidal.δ (AlgebraicGeometry.Scheme.Modules.pullback f) M (M ⟹ F))) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((CategoryTheory.ihom.ev M).app F)) h)

Evaluation after the base-change comparison is the pullback of evaluation, preceded by the inverse canonical tensor comparison. This characterizes the base-change map.

theorem TauCeti.AlgebraicGeometry.pullbackIhomComparison_app_eq_curry {X Y : AlgebraicGeometry.Scheme} (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] (f : X ⟶ Y) (F : Y.Modules) : (pullbackIhomComparison M f).app F = CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Functor.OplaxMonoidal.δ (AlgebraicGeometry.Scheme.Modules.pullback f) M (M ⟹ F))) ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((CategoryTheory.ihom.ev M).app F)))

The base-change comparison is obtained by currying the pullback of evaluation, after inverting the canonical tensor comparison.

theorem TauCeti.AlgebraicGeometry.pullback_map_pre_app_comp_pullbackIhomComparison_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {M₁ M₂ : Y.Modules} [SheafOfModules.IsQuasicoherent M₁] [SheafOfModules.IsQuasicoherent M₂] (g : M₁ ⟶ M₂) (F : Y.Modules) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((CategoryTheory.MonoidalClosed.pre g).app F)) ((pullbackIhomComparison M₁ f).app F) = CategoryTheory.CategoryStruct.comp ((pullbackIhomComparison M₂ f).app F) ((CategoryTheory.MonoidalClosed.pre ((AlgebraicGeometry.Scheme.Modules.pullback f).map g)).app ((AlgebraicGeometry.Scheme.Modules.pullback f).obj F))

The base-change comparison is natural in the quasicoherent source: precomposition with g : M₁ ⟶ M₂ corresponds to precomposition with its pullback.

theorem TauCeti.AlgebraicGeometry.pullback_map_pre_app_comp_pullbackIhomComparison_app_assoc {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {M₁ M₂ : Y.Modules} [SheafOfModules.IsQuasicoherent M₁] [SheafOfModules.IsQuasicoherent M₂] (g : M₁ ⟶ M₂) (F : Y.Modules) {Z : X.Modules} (h : (AlgebraicGeometry.Scheme.Modules.pullback f).obj M₁ ⟹ (AlgebraicGeometry.Scheme.Modules.pullback f).obj F ⟶ Z) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((CategoryTheory.MonoidalClosed.pre g).app F)) (CategoryTheory.CategoryStruct.comp ((pullbackIhomComparison M₁ f).app F) h) = CategoryTheory.CategoryStruct.comp ((pullbackIhomComparison M₂ f).app F) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre ((AlgebraicGeometry.Scheme.Modules.pullback f).map g)).app ((AlgebraicGeometry.Scheme.Modules.pullback f).obj F)) h)

The base-change comparison is natural in the quasicoherent source: precomposition with g : M₁ ⟶ M₂ corresponds to precomposition with its pullback.

theorem TauCeti.AlgebraicGeometry.isIso_pullbackIhomComparison_of_exactPairing {X Y : AlgebraicGeometry.Scheme} (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] (f : X ⟶ Y) (D : Y.Modules) [SheafOfModules.IsQuasicoherent D] [CategoryTheory.ExactPairing D M] : CategoryTheory.IsIso (pullbackIhomComparison M f)

The canonical internal-Hom base-change comparison is invertible for every scheme morphism when its quasicoherent source has a quasicoherent left dual, without any condition on the target.