Sheafify

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

Statistics

Metric	Count
Definitions isGerm, isLocallyGerm, sheafify, sheafifyStalkIso, stalkToFiber, toSheafify	6
Theorems stalkFunctor_map_unit_toSheafify_isIso, stalkToFiber_injective, stalkToFiber_surjective	3
Total	9

TopCat.Presheaf

Definitions

Name	Category	Theorems
sheafify 📖	CompOp	2 math math: stalkToFiber_injective, stalkToFiber_surjective
sheafifyStalkIso 📖	CompOp	—
stalkToFiber 📖	CompOp	2 math math: stalkToFiber_injective, stalkToFiber_surjective
toSheafify 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stalkFunctor_map_unit_toSheafify_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.sheafify TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology CategoryTheory.Functor.map CategoryTheory.toSheafify	—	CategoryTheory.Adjunction.isIso_map_unit_of_isLeftAdjoint_comp CategoryTheory.ObjectProperty.faithful_ι CategoryTheory.ObjectProperty.full_ι
stalkToFiber_injective 📖	mathematical	—	stalk CategoryTheory.types CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self TopCat.Sheaf.presheaf sheafify stalkToFiber	—	TopCat.stalkToFiber_injective CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self germ_eq CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom germ_res CategoryTheory.types_comp_apply
stalkToFiber_surjective 📖	mathematical	—	stalk CategoryTheory.types CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self TopCat.Sheaf.presheaf sheafify stalkToFiber	—	TopCat.stalkToFiber_surjective CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self germ_exist CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom TopCat.PrelocalPredicate.sheafifyOf

TopCat.Presheaf.Sheafify

Definitions

Name	Category	Theorems
isGerm 📖	CompOp	—
isLocallyGerm 📖	CompOp	—

---

← Back to Index