Quasicoherence of internal Hom from a finite locally free sheaf

For a locally free sheaf of finite type M and a quasicoherent sheaf N, the sheaf 𝓗om(M, N) is quasicoherent. The target need not be of finite type. This allows the ordinary sheaf internal Hom from a finite locally free source to restrict to quasicoherent sheaves.

The proof uses the canonical dual-tensor comparison from TauCeti.dualTensorIhom, the finite local freeness of 𝓗om(M, 𝒪) from SheafOfModules.isFiniteLocallyFree_ihom_unit, and closure of quasicoherence under tensor products.

instance SheafOfModules.isQuasicoherent_ihom_of_isLocallyFree {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [M.IsLocallyFree] [M.IsFiniteType] [N.IsQuasicoherent] : (M ⟹ N).IsQuasicoherent

Internal Hom from a locally free sheaf of finite type into a quasicoherent sheaf is quasicoherent. No finiteness hypothesis is required on the target.