Sections of the internal Hom of sheaves of modules

Let R be a sheaf of commutative rings on a small site, and let M and N be sheaves of R-modules. The internal Hom 𝓗om(M, N) of sheaves of modules is defined as the sheafification of the internal Hom of the underlying presheaves of modules (SheafOfModules.ihom_obj). This file shows that the sheafification does nothing: the presheaf internal Hom of two sheaves is already a sheaf. Its sections over U are the morphisms M|_U ⟶ N|_U of restrictions to the slice over U (TauCeti.PresheafOfModules.ihomObjEquiv), and since N is a sheaf, compatible local morphisms of restrictions glue uniquely: under this identification the presheaf internal Hom has the sheaf of local linear morphisms PresheafOfModules.linearHom M N as its underlying presheaf of sets. This needs no sheaf condition on the source M.

Consequently the sections of the sheaf internal Hom are computed exactly as for sheaves of morphisms: a section of 𝓗om(M, N) over U is a morphism of sheaves of modules M.over U ⟶ N.over U, compatibly with restriction and naturally in both M and N. This is the sectionwise description on which the comparison of 𝓗om(M, N) with restriction to a slice rests, for sources M that are only locally free.

Main declarations

• PresheafOfModules.isSheaf_ihom_val: the presheaf internal Hom from any presheaf of modules into a sheaf of modules is a sheaf;
• SheafOfModules.ihomCompForgetIso: the underlying presheaf of the sheaf internal Hom is the presheaf internal Hom, naturally in the source and target;
• SheafOfModules.ihomObjEquiv: the sections of 𝓗om(M, N) over U are the morphisms M.over U ⟶ N.over U; SheafOfModules.ihomObjEquiv_apply reads the morphism attached to a section off the presheaf internal Hom, SheafOfModules.ihomObjEquiv_symm_apply reads the section attached to a morphism off it in the same way, and the equivalence is compatible with restriction by SheafOfModules.ihomObjEquiv_map_app, natural in the target by SheafOfModules.ihomObjEquiv_ihom_map_app, and natural in the source by SheafOfModules.ihomObjEquiv_pre_app_app. Its evaluation formula is SheafOfModules.ihomObjEquiv_apply_app, with additivity and scalar compatibility recorded in SheafOfModules.ihomObjEquiv_add_app and SheafOfModules.ihomObjEquiv_smul_app.

References

• [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Exercise 1.15 (the sheaf 𝓗om(M, N) and its sections).

theorem PresheafOfModules.isSheaf_ihom_val {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M : PresheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R).obj) (N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : CategoryTheory.Presheaf.IsSheaf J ((CategoryTheory.ihom M).obj N.val).presheaf

The presheaf internal Hom from a presheaf of modules into a sheaf of modules is a sheaf: its underlying presheaf of sets is the sheaf of local linear morphisms. No sheaf condition is needed on the source.

noncomputable def SheafOfModules.ihomCompForgetIso {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : (CategoryTheory.ihom M).comp (forget (TauCeti.SheafOfModules.ringCatSheaf R)) ≅ (forget (TauCeti.SheafOfModules.ringCatSheaf R)).comp (CategoryTheory.ihom M.val)

The underlying presheaf of the internal Hom of sheaves of modules is the internal Hom of the underlying presheaves: the sheafification defining the former is an isomorphism, since the latter is already a sheaf (PresheafOfModules.isSheaf_ihom_val).

Equations

• M.ihomCompForgetIso = CategoryTheory.NatIso.ofComponents (TauCeti.SheafOfModules.ihomCompForgetIsoApp✝ M) ⋯

theorem SheafOfModules.ihomCompForgetIso_pre_app {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M' : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (f : M' ⟶ M) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app N).val (M'.ihomCompForgetIso.hom.app N) = CategoryTheory.CategoryStruct.comp (M.ihomCompForgetIso.hom.app N) ((CategoryTheory.MonoidalClosed.pre f.val).app N.val)

The comparison between sheaf and presheaf internal Homs is natural in the source.

noncomputable def SheafOfModules.ihomObjEquiv {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (U : C) : ↑(((CategoryTheory.ihom M).obj N).val.obj (Opposite.op U)) ≃ (M.over U ⟶ N.over U)

The sections over U of the internal Hom 𝓗om(M, N) of sheaves of modules are the morphisms M.over U ⟶ N.over U of restrictions to the slice over U.

Equations

• One or more equations did not get rendered due to their size.

theorem SheafOfModules.ihomObjEquiv_apply {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (U : C) (s : ↑(((CategoryTheory.ihom M).obj N).val.obj (Opposite.op U))) : (M.ihomObjEquiv N U) s = { val := (TauCeti.PresheafOfModules.ihomObjEquiv U M.val N.val) ((CategoryTheory.ConcreteCategory.hom ((M.ihomCompForgetIso.hom.app N).app (Opposite.op U))) s) }

The morphism of restrictions attached to a section of 𝓗om(M, N) is the one attached to its image in the presheaf internal Hom (TauCeti.PresheafOfModules.ihomObjEquiv).

theorem SheafOfModules.ihomObjEquiv_symm_apply {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (U : C) (φ : M.over U ⟶ N.over U) : (M.ihomObjEquiv N U).symm φ = (CategoryTheory.ConcreteCategory.hom ((M.ihomCompForgetIso.inv.app N).app (Opposite.op U))) ((TauCeti.PresheafOfModules.ihomObjEquiv U M.val N.val).symm φ.val)

The section of 𝓗om(M, N) attached to a morphism of restrictions is the image of the section of the presheaf internal Hom attached to it (TauCeti.PresheafOfModules.ihomObjEquiv).

theorem SheafOfModules.ihomObjEquiv_map_app {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {U : C} (s : ↑(((CategoryTheory.ihom M).obj N).val.obj (Opposite.op U))) {V : C} (g : V ⟶ U) {W : C} (h : W ⟶ V) (m : ↑(M.val.obj (Opposite.op W))) : (CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N V) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom M).obj N).val.map g.op)) s)).val.app (Opposite.op (CategoryTheory.Over.mk h)))) m = (CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N U) s).val.app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp h g))))) m

Restricting a section of 𝓗om(M, N) along g : V ⟶ U restricts the corresponding morphism of restrictions to the slice over V.

theorem SheafOfModules.ihomObjEquiv_ihom_map_app {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {N' : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (α : N ⟶ N') (U : C) (s : ↑(((CategoryTheory.ihom M).obj N).val.obj (Opposite.op U))) : (M.ihomObjEquiv N' U) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom M).map α).val.app (Opposite.op U))) s) = CategoryTheory.CategoryStruct.comp ((M.ihomObjEquiv N U) s) (Hom.over α U)

The sections equivalence is natural in the target: applying 𝓗om(M, α) to a section corresponds to postcomposing the morphism of restrictions with the restriction of α.

theorem SheafOfModules.ihomObjEquiv_pre_app_app {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M' : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (β : M' ⟶ M) (U : C) (s : ↑(((CategoryTheory.ihom M).obj N).val.obj (Opposite.op U))) : (M'.ihomObjEquiv N U) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.MonoidalClosed.pre β).app N).val.app (Opposite.op U))) s) = CategoryTheory.CategoryStruct.comp (Hom.over β U) ((M.ihomObjEquiv N U) s)

The sections equivalence is natural in the source: applying Hom(β, N) to a section corresponds to precomposing the morphism of restrictions with the restriction of β.

theorem SheafOfModules.ihomObjEquiv_apply_app {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (U : C) (s : ↑(((CategoryTheory.ihom M).obj N).val.obj (Opposite.op U))) {V : C} (g : V ⟶ U) (m : ↑(M.val.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N U) s).val.app (Opposite.op (CategoryTheory.Over.mk g)))) m = (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((CategoryTheory.ihom.ev M.val).app N.val) (Opposite.op V))) (m ⊗ₜ[↑(R.obj.obj (Opposite.op V))] (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom M.val).obj N.val).map g.op)) ((CategoryTheory.ConcreteCategory.hom ((M.ihomCompForgetIso.hom.app N).app (Opposite.op U))) s))

Evaluating a local internal-Hom section is evaluation in the presheaf internal Hom, after the comparison between the sheaf and presheaf internal Homs.

theorem SheafOfModules.ihomObjEquiv_add_app {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (U : C) (s t : ↑(((CategoryTheory.ihom M).obj N).val.obj (Opposite.op U))) {V : C} (g : V ⟶ U) (m : ↑(M.val.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N U) (s + t)).val.app (Opposite.op (CategoryTheory.Over.mk g)))) m = (CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N U) s).val.app (Opposite.op (CategoryTheory.Over.mk g)))) m + (CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N U) t).val.app (Opposite.op (CategoryTheory.Over.mk g)))) m

Evaluation of a local morphism is additive in its internal-Hom section.

theorem SheafOfModules.ihomObjEquiv_smul_app {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (U : C) (r : ↑(R.obj.obj (Opposite.op U))) (s : ↑(((CategoryTheory.ihom M).obj N).val.obj (Opposite.op U))) {V : C} (g : V ⟶ U) (m : ↑(M.val.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N U) (r • s)).val.app (Opposite.op (CategoryTheory.Over.mk g)))) m = (CategoryTheory.ConcreteCategory.hom (R.obj.map g.op)) r • (CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N U) s).val.app (Opposite.op (CategoryTheory.Over.mk g)))) m

Evaluation of a scalar multiple of a local morphism multiplies its value by the restricted scalar.