Zulip Chat Archive

Stream: new members

Topic: induced map on stalks


view this post on Zulip Justus Springer (Mar 24 2021 at 15:42):

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 fx ⁣:FxGx f_x\colon \mathcal F_x \rightarrow \mathcal G_x on the stalks for a map of (pre)sheaves f ⁣:FGf\colon \mathcal F\rightarrow \mathcal G over a fixed topological space XX. 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, ff is an isomorphism if and only if all the fxf_x are isomorphisms. I reckon this fits best in topology/sheaves/stalks. Would this be something worth a PR?

view this post on Zulip Johan Commelin (Mar 24 2021 at 15:43):

Certainly worth a PR!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 07 2021 at 19:09):

Thanks a lot for working on this!

view this post on Zulip 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