Sheafify

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

Statistics

Metric	Count
Definitions isGerm, isLocallyGerm, sheafify, sheafifyStalkIso, stalkToFiber, toSheafify	6
Theorems stalkToFiber_injective, stalkToFiber_surjective	2
Total	8

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
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