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 instCategorySheaf hasFilteredColimitsOfSize	—	hasFilteredColimitsOfSize CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits hasExactColimitsOfShape CategoryTheory.AB5OfSize.ofShape
hasExactColimitsOfShape 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Sheaf instCategorySheaf instHasColimitsOfShape CategoryTheory.instHasWeakSheafifyOfHasSheafify	—	CategoryTheory.Adjunction.hasExactColimitsOfShape CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf CategoryTheory.Limits.functorCategoryHasColimitsOfShape instHasColimitsOfShape CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits instHasFiniteLimits CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf
hasFilteredColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasFilteredColimitsOfSize CategoryTheory.Sheaf instCategorySheaf	—	instHasColimitsOfShape CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits
instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Sheaf instCategorySheaf instHasColimitsOfShape	—	CategoryTheory.HasExactColimitsOfShape.domain_of_functor instHasColimitsOfShape CategoryTheory.Limits.functorCategoryHasColimitsOfShape CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf instHasFiniteLimits
instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Sheaf instCategorySheaf instHasLimitsOfShape	—	CategoryTheory.HasExactLimitsOfShape.domain_of_functor instHasLimitsOfShape CategoryTheory.Limits.functorCategoryHasLimitsOfShape CategoryTheory.instHasExactLimitsOfShapeFunctorOfHasFiniteColimits CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf instHasFiniteColimits CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint
instIsGrothendieckAbelian 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian CategoryTheory.Sheaf instCategorySheaf CategoryTheory.sheafIsAbelian	—	CategoryTheory.locallySmall_of_univLE UnivLE.self hasFilteredColimitsOfSize CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize ab5ofSize CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits CategoryTheory.IsGrothendieckAbelian.hasLimits CategoryTheory.IsGrothendieckAbelian.ab5OfSize hasSeparator CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.IsGrothendieckAbelian.hasColimits CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.IsGrothendieckAbelian.hasSeparator
isGrothendieckAbelian_of_essentiallySmall 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian CategoryTheory.Sheaf instCategorySheaf 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 CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits CategoryTheory.Limits.hasCofilteredLimitsOfSize_of_hasLimitsOfSize CategoryTheory.IsGrothendieckAbelian.hasLimits CategoryTheory.RepresentablyFlat.cofiltered CategoryTheory.instRepresentablyFlatOppositeOpOfRepresentablyCoflat CategoryTheory.RepresentablyCoflat.of_isLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence

---

← Back to Index