The stalk comparison for internal Hom

A germ of a local morphism of sheaves of modules acts on germs of sections. This gives the canonical linear comparison from the stalk of the internal Hom to the module of linear maps between the two stalks, naturally in both sheaves. No finiteness hypothesis is imposed on the source, and the comparison is not asserted to be invertible.

The construction uses Mathlib's module structure on stalks and its filtered-colimit universal property, together with the sectionwise description of internal Hom in InternalHom.Basic.

Main declarations

• SheafOfModules.ihomStalkComparison: the comparison as a linear map over the ring stalk;
• SheafOfModules.ihomStalkComparison_germ_apply: evaluation on representatives in a neighborhood;
• SheafOfModules.ihomStalkComparison_naturality and SheafOfModules.ihomStalkComparison_pre: compatibility with morphisms in the target and source.

noncomputable def SheafOfModules.ihomStalkComparison {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (x : ↑X) : ↑(TopCat.Presheaf.stalk (M ⟹ N).val.presheaf x) →ₗ[↑(TopCat.Presheaf.stalk R.obj x)] ↑(TopCat.Presheaf.stalk M.val.presheaf x) →ₗ[↑(TopCat.Presheaf.stalk R.obj x)] ↑(TopCat.Presheaf.stalk N.val.presheaf x)

The canonical linear comparison from the stalk of the internal Hom to linear maps between stalks, obtained by letting germs of local morphisms act on germs of sections.

Equations

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

theorem SheafOfModules.ihomStalkComparison_germ {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (x : ↑X) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (s : ↑((M ⟹ N).val.obj (Opposite.op U))) : ((M.ihomStalkComparison N x) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ (M ⟹ N).val.presheaf U x hx)) s)).toAddHom = (M.val.stalkMapOver x U ((M.ihomObjEquiv N U) s).val hx).toAddHom

On a germ of a local internal-Hom section, the comparison has the underlying additive map of the stalk map of its local morphism. The two linear maps use respectively the original commutative-ring stalk and the stalk after forgetting commutativity as their scalar rings.

theorem SheafOfModules.ihomStalkComparison_germ_apply {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (x : ↑X) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (s : ↑((M ⟹ N).val.obj (Opposite.op U))) (V : TopologicalSpace.Opens ↑X) (i : V ⟶ U) (hxV : x ∈ V) (m : ↑(M.val.obj (Opposite.op V))) : ((M.ihomStalkComparison N x) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ (M ⟹ N).val.presheaf U x hx)) s)) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.val.presheaf V x hxV)) m) = (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N.val.presheaf V x hxV)) ((CategoryTheory.ConcreteCategory.hom (((M.ihomObjEquiv N U) s).val.app (Opposite.op (CategoryTheory.Over.mk i)))) m)

The comparison evaluates two germs by applying the local morphism to a representative section in its domain.

theorem SheafOfModules.ihomStalkComparison_naturality {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (x : ↑X) {N' : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (α : N ⟶ N') (s : ↑(TopCat.Presheaf.stalk (M ⟹ N).val.presheaf x)) (m : ↑(TopCat.Presheaf.stalk M.val.presheaf x)) : ((M.ihomStalkComparison N' x) ((CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).map ((PresheafOfModules.toPresheaf (TauCeti.SheafOfModules.ringCatSheaf R).obj).map ((CategoryTheory.ihom M).map α).val))) s)) m = (CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).map ((PresheafOfModules.toPresheaf (TauCeti.SheafOfModules.ringCatSheaf R).obj).map α.val))) (((M.ihomStalkComparison N x) s) m)

The stalk comparison is covariant in the target: a morphism of target sheaves acts by postcomposition with its stalk map.

theorem SheafOfModules.ihomStalkComparison_pre {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (x : ↑X) {M' : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (β : M' ⟶ M) (s : ↑(TopCat.Presheaf.stalk (M ⟹ N).val.presheaf x)) (m : ↑(TopCat.Presheaf.stalk M'.val.presheaf x)) : ((M'.ihomStalkComparison N x) ((CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).map ((PresheafOfModules.toPresheaf (TauCeti.SheafOfModules.ringCatSheaf R).obj).map ((CategoryTheory.MonoidalClosed.pre β).app N).val))) s)) m = ((M.ihomStalkComparison N x) s) ((CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).map ((PresheafOfModules.toPresheaf (TauCeti.SheafOfModules.ringCatSheaf R).obj).map β.val))) m)

The stalk comparison is contravariant in the source: a morphism of source sheaves acts by precomposition with its stalk map.