The internal-Hom stalk comparison for finitely presented sources

Let M and N be sheaves of modules over a sheaf of commutative rings on a topological space. If M is finitely presented, the canonical comparison 𝓗om(M, N)ₓ ⟶ Hom(Mₓ, Nₓ) from the stalk of the internal Hom to linear maps between the stalks is bijective, for an arbitrary target N. Injectivity only needs M to be of finite type and is SheafOfModules.ihomStalkComparison_injective; this file supplies surjectivity and packages the comparison as a linear equivalence.

For surjectivity, let φ : Mₓ → Nₓ be linear and choose a finite presentation of M on a neighbourhood U of x. The images under φ of the germs of the generators are germs of sections of N on a smaller neighbourhood. The relations hold among these sections at the level of germs, hence on a still smaller neighbourhood V, so the sections define a morphism M|_V ⟶ N|_V through the cokernel description of the restricted presentation. Its germ maps to φ, because both agree on the germs of the generators, which span Mₓ.

Without finite presentation the comparison need not be surjective, so no such statement is made for sources that are only of finite type.

Main declarations

• SheafOfModules.ihomStalkComparison_surjective: surjectivity for finitely presented sources;
• SheafOfModules.ihomStalkComparison_bijective: bijectivity for finitely presented sources;
• SheafOfModules.ihomStalkEquiv: the comparison as a linear equivalence 𝓗om(M, N)ₓ ≃ Hom(Mₓ, Nₓ).

References

• The Stacks Project, Tag 01CP.

theorem SheafOfModules.ihomStalkComparison_surjective {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [M.IsFinitePresentation] (x : ↑X) : Function.Surjective ⇑(M.ihomStalkComparison N x)

For a finitely presented source sheaf, every linear map between stalks is the image of a germ of a local morphism. No condition is imposed on the target.

theorem SheafOfModules.ihomStalkComparison_bijective {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [M.IsFinitePresentation] (x : ↑X) : Function.Bijective ⇑(M.ihomStalkComparison N x)

For a finitely presented source sheaf, the comparison from the stalk of the internal Hom to linear maps between the stalks is bijective.

noncomputable def SheafOfModules.ihomStalkEquiv {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [M.IsFinitePresentation] (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)

For a finitely presented source sheaf M, the stalk at x of the internal Hom 𝓗om(M, N) is the module of linear maps from the stalk of M to the stalk of N, through the canonical comparison SheafOfModules.ihomStalkComparison.

Equations

• M.ihomStalkEquiv N x = LinearEquiv.ofBijective (M.ihomStalkComparison N x) ⋯

theorem SheafOfModules.ihomStalkEquiv_apply {X : TopCat} {R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [M.IsFinitePresentation] (x : ↑X) (s : ↑(TopCat.Presheaf.stalk (M ⟹ N).val.presheaf x)) : (M.ihomStalkEquiv N x) s = (M.ihomStalkComparison N x) s

The stalk equivalence is the canonical comparison.