# Zulip Chat Archive

## Stream: new members

### Topic: induced map on stalks

#### 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 $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 (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