Sheaf

📁 Source: Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean

Statistics

Metric	Count
Definitions	0
Theorems ab5ofSize, hasExactColimitsOfShape, hasFilteredColimitsOfSize, instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf, instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf, instIsGrothendieckAbelian, isGrothendieckAbelian_of_essentiallySmall	7
Total	7

CategoryTheory.Sheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ab5ofSize 📖	mathematical	—	CategoryTheory.AB5OfSize CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf hasFilteredColimitsOfSize	—	hasFilteredColimitsOfSize CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits hasExactColimitsOfShape CategoryTheory.AB5OfSize.ofShape
hasExactColimitsOfShape 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf instHasColimitsOfShape CategoryTheory.instHasWeakSheafifyOfHasSheafify	—	CategoryTheory.Adjunction.hasExactColimitsOfShape CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι CategoryTheory.Limits.functorCategoryHasColimitsOfShape instHasColimitsOfShape CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits instHasFiniteLimits CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf
hasFilteredColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasFilteredColimitsOfSize CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	instHasColimitsOfShape CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits
instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf instHasColimitsOfShape	—	CategoryTheory.HasExactColimitsOfShape.domain_of_functor instHasColimitsOfShape CategoryTheory.Limits.functorCategoryHasColimitsOfShape CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι instHasFiniteLimits
instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf instHasLimitsOfShape	—	CategoryTheory.HasExactLimitsOfShape.domain_of_functor instHasLimitsOfShape CategoryTheory.Limits.functorCategoryHasLimitsOfShape CategoryTheory.instHasExactLimitsOfShapeFunctorOfHasFiniteColimits CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι instHasFiniteColimits CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint
instIsGrothendieckAbelian 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafIsAbelian	—	CategoryTheory.locallySmall_fullSubcategory CategoryTheory.instLocallySmallFunctor CategoryTheory.IsGrothendieckAbelian.locallySmall hasFilteredColimitsOfSize CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize ab5ofSize CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.IsGrothendieckAbelian.ab5OfSize hasSeparator CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.IsGrothendieckAbelian.hasColimits CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.IsGrothendieckAbelian.hasSeparator
isGrothendieckAbelian_of_essentiallySmall 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite CategoryTheory.SmallModel CategoryTheory.Category.opposite CategoryTheory.smallCategorySmallModel CategoryTheory.Functor.op CategoryTheory.Equivalence.inverse CategoryTheory.equivSmallModel CategoryTheory.instCategoryStructuredArrow	CategoryTheory.IsGrothendieckAbelian CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafIsAbelian CategoryTheory.hasSheafifyEssentiallySmallSite	—	CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Equivalence.faithful_inverse CategoryTheory.IsGrothendieckAbelian.of_equivalence CategoryTheory.hasSheafifyEssentiallySmallSite instIsGrothendieckAbelian

---

← Back to Index