induced map on stalks

Stream: new members

[Justus Springer]

Hello!
I've been learning Lean an playing around with parts of the mathlib library for some time now, and I would like to start contributing. As a starter project, I would like to formalize and develop some API for the concept of the induced morphism $f_x\colon \mathcal F_x \rightarrow \mathcal G_x$ on the stalks for a map of (pre)sheaves $f\colon \mathcal F\rightarrow \mathcal G$ over a fixed topological space $X$. In algebraic_geometry/stalks.lean, this has already been defined for presheaved spaces, which can be realized as a special case where one of the sheaves is the pushforward of a structure presheaf. Furthermore, I would like to formalize the statement that, for sheaves, $f$ is an isomorphism if and only if all the $f_x$ are isomorphisms. I reckon this fits best in topology/sheaves/stalks. Would this be something worth a PR?

[Johan Commelin]

Certainly worth a PR!

[Justus Springer]

Well, it obviously took longer than I expected, but after some preparatory PRs, this is now done: #7092

[Johan Commelin]

Thanks a lot for working on this!

[Johan Commelin]

I've wanted to push for some progress here for quite some time. But there was always a lot of other stuff on my todo list.