Stream: new members
Topic: induced map on stalks
Justus Springer (Mar 24 2021 at 15:42):
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 on the stalks for a map of (pre)sheaves over a fixed topological space . 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, is an isomorphism if and only if all the are isomorphisms. I reckon this fits best in
topology/sheaves/stalks. Would this be something worth a PR?
Johan Commelin (Mar 24 2021 at 15:43):
Certainly worth a PR!
Justus Springer (Apr 07 2021 at 19:07):
Well, it obviously took longer than I expected, but after some preparatory PRs, this is now done: #7092
Johan Commelin (Apr 07 2021 at 19:09):
Thanks a lot for working on this!
Johan Commelin (Apr 07 2021 at 19:10):
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.
Last updated: May 12 2021 at 05:19 UTC