Commit 2021-06-02 04:57 cdf6cf0f

View on Github →

feat(topology/sheaves/stalks): Small lemmas about stalk pushforward and stalk map (#7789) Top.presheaf.stalk_pushforward and PresheafedSpace.stalk_map commute with Top.presheaf.germ.

Estimated changes

Modified src/algebraic_geometry/stalks.lean

added theorem algebraic_geometry.PresheafedSpace.stalk_map_germ

Modified src/topology/sheaves/stalks.lean

added theorem Top.presheaf.stalk_pushforward_germ