Commit 2023-05-30 09:11 e9ab1b47

View on Github →

feat: port Topology.Sheaves.Stalks (#4449)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/Stalks.lean

added theorem TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective

added theorem TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective

added theorem TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective

added theorem TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso

added theorem TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective

added theorem TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective

added def TopCat.Presheaf.germ

added def TopCat.Presheaf.germToPullbackStalk

added theorem TopCat.Presheaf.germ_eq

added theorem TopCat.Presheaf.germ_exist

added theorem TopCat.Presheaf.germ_ext

added theorem TopCat.Presheaf.germ_res

added theorem TopCat.Presheaf.germ_stalkSpecializes

added theorem TopCat.Presheaf.germ_stalk_specializes'

added theorem TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso

added theorem TopCat.Presheaf.isIso_of_stalkFunctor_map_iso

added theorem TopCat.Presheaf.mono_iff_stalk_mono

added theorem TopCat.Presheaf.mono_of_stalk_mono

added theorem TopCat.Presheaf.section_ext

added def TopCat.Presheaf.stalk

added def TopCat.Presheaf.stalkCongr

added def TopCat.Presheaf.stalkFunctor

added theorem TopCat.Presheaf.stalkFunctor_map_germ

added theorem TopCat.Presheaf.stalkFunctor_map_injective_of_app_injective

added theorem TopCat.Presheaf.stalkFunctor_obj

added def TopCat.Presheaf.stalkPullbackHom

added def TopCat.Presheaf.stalkPullbackInv

added def TopCat.Presheaf.stalkPullbackIso

added theorem TopCat.Presheaf.stalkPushforward.comp

added theorem TopCat.Presheaf.stalkPushforward.id

added theorem TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_openEmbedding

added def TopCat.Presheaf.stalkPushforward

added theorem TopCat.Presheaf.stalkPushforward_germ

added theorem TopCat.Presheaf.stalkSpecializes_comp

added theorem TopCat.Presheaf.stalkSpecializes_refl

added theorem TopCat.Presheaf.stalkSpecializes_stalkFunctor_map

added theorem TopCat.Presheaf.stalkSpecializes_stalkPushforward

added theorem TopCat.Presheaf.stalk_hom_ext

added theorem TopCat.Presheaf.stalk_mono_of_mono

added theorem TopCat.Presheaf.stalk_open_algebraMap