ExtensiveColimits

📁 Source: Mathlib/CategoryTheory/Sites/Coherent/ExtensiveColimits.lean

Statistics

Metric	Count
Definitions	0
Theorems instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, instPreservesFiniteProductsFunctorColimOfPreadditive, isSheaf_pointwiseColimit	4
Total	4

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim 📖	mathematical	—	Limits.PreservesColimitsOfShape Sheaf extensiveTopology FinitaryExtensive.toFinitaryPreExtensive Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category sheafToPresheaf	—	FinitaryExtensive.toFinitaryPreExtensive Presheaf.isSheaf_of_iso_iff isSheaf_pointwiseColimit preservesColimit_of_createsColimit_and_hasColimit Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape
instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits 📖	mathematical	—	Limits.PreservesFiniteColimits Sheaf extensiveTopology FinitaryExtensive.toFinitaryPreExtensive Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category sheafToPresheaf	—	FinitaryExtensive.toFinitaryPreExtensive instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim Limits.hasColimitsOfShape_of_hasFiniteColimits instPreservesFiniteProductsFunctorColimOfPreadditive
instPreservesFiniteProductsFunctorColimOfPreadditive 📖	mathematical	—	Limits.PreservesFiniteProducts Functor Functor.category Limits.colim	—	Limits.preservesProductsOfShape_of_preservesBiproductsOfShape Functor.preservesZeroMorphisms_of_isLeftAdjoint Limits.instIsLeftAdjointFunctorColim Finite.of_fintype Limits.preservesBiproductsOfShape_of_preservesCoproductsOfShape Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint
isSheaf_pointwiseColimit 📖	mathematical	—	Presheaf.IsSheaf extensiveTopology FinitaryExtensive.toFinitaryPreExtensive Limits.Cocone.pt Functor Opposite Category.opposite Functor.category Functor.comp Sheaf Sheaf.instCategorySheaf sheafToPresheaf Limits.pointwiseCocone	—	FinitaryExtensive.toFinitaryPreExtensive Presheaf.isSheaf_iff_preservesFiniteProducts Limits.comp_preservesFiniteProducts Sheaf.cond Limits.preservesLimitsOfShape_of_evaluation Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype

---

← Back to Index