Presheaf

📁 Source: Mathlib/CategoryTheory/Subobject/Presheaf.lean

Statistics

Metric	Count
Definitions presheaf	1
Theorems presheaf_map, presheaf_obj	2
Total	3

Subobject

Definitions

Name	Category	Theorems
presheaf 📖	CompOp	5 math math: CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀, presheaf_obj, CategoryTheory.Classifier.SubobjectRepresentableBy.homEquiv_eq, CategoryTheory.isRepresentable_hasClassifier_iff, presheaf_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presheaf_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types presheaf CategoryTheory.Functor.obj CategoryTheory.Subobject Opposite.unop Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
presheaf_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types presheaf CategoryTheory.Subobject Opposite.unop	—	—

---

← Back to Index