LocallySurjective

📁 Source: Mathlib/Topology/Sheaves/LocallySurjective.lean

Statistics

Metric	Count
Definitions IsLocallySurjective	1
Theorems isLocallySurjective_iff, locally_surjective_iff_surjective_on_stalks, isLocallySurjective_iff_epi	3
Total	4

TopCat.Presheaf

Definitions

Name	Category	Theorems
IsLocallySurjective 📖	MathDef	3 math math: locally_surjective_iff_surjective_on_stalks, isLocallySurjective_iff, TopCat.Sheaf.isLocallySurjective_iff_epi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallySurjective_iff 📖	mathematical	—	IsLocallySurjective TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app restrictOpen SetLike.instMembership TopologicalSpace.Opens.instSetLike	—	CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem CategoryTheory.leOfHom
locally_surjective_iff_surjective_on_stalks 📖	mathematical	—	IsLocallySurjective CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	—	germ_exist CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem stalkFunctor_map_germ_apply' germ_res_apply germ_eq stalkFunctor_map_germ_apply CategoryTheory.NatTrans.naturality

TopCat.Sheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallySurjective_iff_epi 📖	mathematical	—	TopCat.Presheaf.IsLocallySurjective CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opens.grothendieckTopology CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Epi TopCat.Sheaf TopCat.instCategorySheaf	—	CategoryTheory.Sheaf.isLocallySurjective_iff_epi'

---

← Back to Index