Stalk of a sheaf of modules

Stream: Is there code for X?

[Raphael Douglas Giles]

If one has a sheaf of $O_X$ modules F, then the stalk of F at some point z should be a module over the stalk of $O_X$ at z (this should also be true for a more general sheaf of rings). I feel like this statement should have a very simple one line proof or even be proven by typeclass inference, but such a proof is not coming to me. Can anyone think of a slick way to show this?

[Kevin Buzzard]

Pedantic remark: this isn't a proof, this involves data (and in particular one has to watch out for diamonds). Can you state what you want in lean?

[Raphael Douglas Giles]

Sure, sorry I should have been more specific. I would like to have the following instance:

instance instModuleSheafOfModulesStalk {X : Scheme.{u}} (F : X.Modules) (x : X) :
    Module (X.presheaf.stalk x) (TopCat.Presheaf.stalk F.val.presheaf x).carrier := sorry

[Bryan Wang]

Probably you would want to use the functoriality of taking stalks docs#stalkFunctor_obj, but I think you would need a trick to get an easy 'proof', since we're essentially saying "something is a module over a colimit" which I haven't seen much of in mathlib?

[Andrew Yang]

cf #14412 but I don't think the author is active anymore

[Kevin Buzzard]

They've got a job doing Lean at a tech company so probably have very little time for mathlib right now.