Sections of the internal Hom of presheaves of modules

Let R be a presheaf of commutative rings on a small category C, and let M and N be presheaves of R-modules. The internal Hom 𝓗om(M, N) of presheaves of modules is only characterized by the tensor--Hom adjunction (it is produced by the adjoint functor theorem in TauCeti.PresheafOfModules.monoidalClosed). This file computes its sections: a section of 𝓗om(M, N) over U is a morphism of presheaves of modules M|_U ⟶ N|_U on the slice over U, where restriction to the slice is PresheafOfModulesOfCommRing.pushforward₀ (Over.forget U) R.

By Mathlib's PresheafOfModules.freeYonedaEquiv, a section over U is a morphism out of the free presheaf of modules TauCeti.PresheafOfModules.freeYoneda R U on the presheaf represented by U; by the tensor--Hom adjunction it is a morphism M ⊗ freeYoneda R U ⟶ N; and by the restriction--extension correspondence TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv these are the morphisms of restrictions. The identification is compatible with restriction along morphisms of C and natural in both arguments. This is the sectionwise description of the internal Hom which restriction and stalk comparisons of internal Homs of sheaves of modules rest on.

As a first application, restriction to a slice commutes with internal Hom. Restriction pushforward₀ (Over.forget X) R is a monoidal functor, so it has a canonical comparison 𝓗om(M, N)|_X ⟶ 𝓗om(M|_X, N|_X) (CategoryTheory.Functor.ihomComparison). Over an object Y of the slice over X, both sides have sections identified with morphisms of restrictions: to the slice over Y.left of C on the left, and to the iterated slice over Y on the right. Under these identifications the comparison is restriction along Mathlib's iterated-slice equivalence Over.iteratedSliceEquiv Y, so it is bijective on sections, and the comparison is an isomorphism for every M, with no finiteness condition.

Main declarations

• TauCeti.PresheafOfModules.ihomObjEquiv: the sections of 𝓗om(M, N) over U are the morphisms M|_U ⟶ N|_U, characterized by TauCeti.PresheafOfModules.ihomObjEquiv_apply_app (a section acts by evaluation of its restrictions), compatible with restriction along morphisms of C by TauCeti.PresheafOfModules.ihomObjEquiv_map_app, and natural in the target and in the source by TauCeti.PresheafOfModules.ihomObjEquiv_ihom_map_app and TauCeti.PresheafOfModules.ihomObjEquiv_pre_app_app;
• TauCeti.PresheafOfModules.ihomObjEquiv_ihomComparison_natTrans_app_app: on sections, the internal Hom comparison for restriction to a slice is restriction along the iterated-slice equivalence;
• TauCeti.PresheafOfModules.isIso_ihomComparison_pushforward₀_overForget: restriction to a slice commutes with internal Hom.

References

• [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Exercise 1.15, for the sectionwise description of sheaf Hom which this file establishes for the categorical internal Hom of presheaves of modules.

noncomputable def TauCeti.PresheafOfModules.ihomObjEquiv {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) : ↑(((CategoryTheory.ihom M).obj N).obj (Opposite.op U)) ≃ ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj N)

The sections over U of the internal Hom 𝓗om(M, N) are the morphisms of presheaves of modules M|_U ⟶ N|_U on the slice over U: a section corresponds to a morphism out of the free presheaf represented by U, hence, by the tensor--Hom adjunction, to a morphism out of M ⊗ freeYoneda R U, and these are the morphisms of restrictions.

Equations

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

theorem TauCeti.PresheafOfModules.ihomObjEquiv_apply {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (s : ↑(((CategoryTheory.ihom M).obj N).obj (Opposite.op U))) : (ihomObjEquiv U M N) s = restrictOfTensorFreeYoneda U M N (CategoryTheory.MonoidalClosed.uncurry (PresheafOfModules.freeYonedaEquiv.symm s))

The morphism of restrictions corresponding to a section of 𝓗om(M, N) is obtained by uncurrying the corresponding morphism out of the free presheaf represented by U and restricting.

theorem TauCeti.PresheafOfModules.ihomObjEquiv_symm_apply {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (φ : (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj N) : (ihomObjEquiv U M N).symm φ = PresheafOfModules.freeYonedaEquiv (CategoryTheory.MonoidalClosed.curry (tensorFreeYonedaOfRestrict U M N φ))

The section of 𝓗om(M, N) corresponding to a morphism of restrictions is obtained by extending it to the tensor product with the free presheaf represented by U and currying.

theorem TauCeti.PresheafOfModules.ihomObjEquiv_apply_app {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (s : ↑(((CategoryTheory.ihom M).obj N).obj (Opposite.op U))) {V : C} (g : V ⟶ U) (m : ↑(M.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((ihomObjEquiv U M N) s) (Opposite.op (CategoryTheory.Over.mk g)))) m = (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((CategoryTheory.ihom.ev M).app N) (Opposite.op V))) (m ⊗ₜ[↑(R.obj (Opposite.op V))] (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom M).obj N).map g.op)) s)

The morphism of restrictions corresponding to a section s of 𝓗om(M, N) over U acts at g : V ⟶ U by evaluating the restriction of s along g.

This is not a simp lemma, for the same reason as TauCeti.PresheafOfModules.restrictOfTensorFreeYoneda_app_apply: simp rewrites the base ring of the component inside the implicit arguments of the coercion.

theorem TauCeti.PresheafOfModules.ihomObjEquiv_map_app {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (s : ↑(((CategoryTheory.ihom M).obj N).obj (Opposite.op U))) {V : C} (g : V ⟶ U) {W : C} (h : W ⟶ V) (m : ↑(M.obj (Opposite.op W))) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((ihomObjEquiv V M N) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom M).obj N).map g.op)) s)) (Opposite.op (CategoryTheory.Over.mk h)))) m = (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((ihomObjEquiv U M N) s) (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 TauCeti.PresheafOfModules.ihomObjEquiv_ihom_map_app {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) {N' : PresheafOfModulesOfCommRing R} (α : N ⟶ N') (s : ↑(((CategoryTheory.ihom M).obj N).obj (Opposite.op U))) : (ihomObjEquiv U M N') ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom M).map α).app (Opposite.op U))) s) = CategoryTheory.CategoryStruct.comp ((ihomObjEquiv U M N) s) ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).map α)

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 TauCeti.PresheafOfModules.ihomObjEquiv_pre_app_app {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) {M' : PresheafOfModulesOfCommRing R} (β : M' ⟶ M) (s : ↑(((CategoryTheory.ihom M).obj N).obj (Opposite.op U))) : (ihomObjEquiv U M' N) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.MonoidalClosed.pre β).app N).app (Opposite.op U))) s) = CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).map β) ((ihomObjEquiv U M N) s)

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

theorem TauCeti.PresheafOfModules.ihomObjEquiv_ihomComparison_natTrans_app_app {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : C) (M N : PresheafOfModulesOfCommRing R) (Y : CategoryTheory.Over X) (s : ↑(((CategoryTheory.ihom M).obj N).obj (Opposite.op Y.left))) : (ihomObjEquiv Y ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget X) R).obj M) ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget X) R).obj N)) ((CategoryTheory.ConcreteCategory.hom ((((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget X) R).ihomComparison M).natTrans.app N).app (Opposite.op Y))) s) = (PresheafOfModulesOfCommRing.pushforward₀ Y.iteratedSliceForward ((CategoryTheory.Over.forget Y.left).op.comp R)).map ((ihomObjEquiv Y.left M N) s)

On sections over Y, the internal Hom comparison for restriction to the slice over X is restriction along the iterated-slice equivalence: a section of 𝓗om(M, N) over Y.left, viewed as a morphism M|_{Y.left} ⟶ N|_{Y.left}, is sent to the section of 𝓗om(M|_X, N|_X) over Y given by the same morphism on the iterated slice over Y.

instance TauCeti.PresheafOfModules.isIso_ihomComparison_pushforward₀_overForget {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : C) (M : PresheafOfModulesOfCommRing R) : CategoryTheory.IsIso ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget X) R).ihomComparison M).natTrans

Restriction to the slice over X commutes with internal Hom: the canonical comparison 𝓗om(M, N)|_X ⟶ 𝓗om(M|_X, N|_X) is an isomorphism for every presheaf of modules M.