Commit 2021-04-14 18:40 3df0f773

View on Github →

feat(topology/sheaves): Induced map on stalks (#7092) This PR defines stalk maps for morphisms of presheaves. We prove that a morphism of type-valued sheaves is an isomorphism if and only if all the stalk maps are isomorphisms. A few more lemmas about unique gluing are also added, as well as docstrings.

Estimated changes

Modified src/topology/sheaves/sheaf_condition/equalizer_products.lean

added theorem Top.presheaf.sheaf_condition_equalizer_products.res_π

Modified src/topology/sheaves/sheaf_condition/unique_gluing.lean

added theorem Top.presheaf.res_π_apply

added theorem Top.sheaf.eq_of_locally_eq'

added theorem Top.sheaf.eq_of_locally_eq

added theorem Top.sheaf.exists_unique_gluing'

Modified src/topology/sheaves/stalks.lean

added theorem Top.presheaf.app_bijective_of_stalk_functor_map_bijective

added theorem Top.presheaf.app_injective_iff_stalk_functor_map_injective

added theorem Top.presheaf.app_injective_of_stalk_functor_map_injective

added theorem Top.presheaf.is_iso_iff_stalk_functor_map_iso

added theorem Top.presheaf.is_iso_of_stalk_functor_map_iso

added theorem Top.presheaf.section_ext

added theorem Top.presheaf.stalk_functor_map_germ

added theorem Top.presheaf.stalk_functor_map_germ_apply

added theorem Top.presheaf.stalk_functor_map_injective_of_app_injective