Limits

📁 Source: Mathlib/CategoryTheory/Sites/Limits.lean

Statistics

Metric	Count
Definitions createsColimitOfIsSheaf, createsLimits, createsLimitsOfShape, instCreatesLimitFunctorOppositeSheafToPresheaf, isColimitSheafifyCocone, isLimitMultiforkOfIsLimit, multiforkEvaluationCone, sheafifyCocone	8
Theorems hasLimitsOfSize, instHasColimitsOfShape, instHasColimitsOfSize, instHasFiniteColimits, instHasFiniteCoproducts, instHasFiniteLimits, instHasFiniteProducts, instHasLimitsOfShape, instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits, isSheaf_of_isLimit, sheafifyCocone_ι_app_val, sheafifyCocone_ι_app_val_assoc	12
Total	20

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
createsColimitOfIsSheaf 📖	CompOp	—
createsLimits 📖	CompOp	—
createsLimitsOfShape 📖	CompOp	—
instCreatesLimitFunctorOppositeSheafToPresheaf 📖	CompOp	—
isColimitSheafifyCocone 📖	CompOp	—
isLimitMultiforkOfIsLimit 📖	CompOp	—
multiforkEvaluationCone 📖	CompOp	—
sheafifyCocone 📖	CompOp	2 math math: sheafifyCocone_ι_app_val_assoc, sheafifyCocone_ι_app_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CategoryTheory.Sheaf instCategorySheaf	—	CategoryTheory.hasLimits_of_hasLimits_createsLimits CategoryTheory.Limits.functorCategoryHasLimitsOfSize
instHasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Sheaf instCategorySheaf	—	CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instHasColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize CategoryTheory.Sheaf instCategorySheaf	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
instHasFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits CategoryTheory.Sheaf instCategorySheaf	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits
instHasFiniteCoproducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteCoproducts CategoryTheory.Sheaf instCategorySheaf	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype
instHasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits CategoryTheory.Sheaf instCategorySheaf	—	instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
instHasFiniteProducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteProducts CategoryTheory.Sheaf instCategorySheaf	—	instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype
instHasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Sheaf instCategorySheaf	—	CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape CategoryTheory.Limits.functorCategoryHasLimitsOfShape
instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Sheaf instCategorySheaf CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.sheafToPresheaf	—	CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.functorCategoryHasLimitsOfShape
isSheaf_of_isLimit 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Limits.Cone.pt CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Sheaf instCategorySheaf CategoryTheory.sheafToPresheaf	—	CategoryTheory.Presheaf.isSheaf_iff_multifork
sheafifyCocone_ι_app_val 📖	mathematical	—	Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt sheafifyCocone CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.sheafToPresheaf CategoryTheory.sheafify CategoryTheory.toSheafify	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.isIso_sheafificationAdjunction_counit CategoryTheory.sheafification_reflective comp_val_assoc CategoryTheory.NatTrans.comp_app CategoryTheory.IsIso.hom_inv_id CategoryTheory.NatTrans.id_app CategoryTheory.Category.id_comp CategoryTheory.toSheafify_naturality cond CategoryTheory.sheafificationAdjunction_counit_app_val CategoryTheory.sheafifyLift_id_toSheafify_assoc
sheafifyCocone_ι_app_val_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category val CategoryTheory.Functor.obj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt sheafifyCocone Hom.val CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Functor.comp CategoryTheory.sheafToPresheaf CategoryTheory.toSheafify	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sheafifyCocone_ι_app_val

---

← Back to Index