IsStack

📁 Source: Mathlib/CategoryTheory/Sites/Descent/IsStack.lean

Statistics

Metric	Count
Definitions IsStack	1
Theorems essSurj_of_sieve, of_isStackFor, toIsPrestack, isEquivalence_toDescentData, isStackFor, isStackFor'	6
Total	7

CategoryTheory.Pseudofunctor

Definitions

Name	Category	Theorems
IsStack 📖	CompData	2 math math: IsStack.of_precoverage, IsStack.of_isStackFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEquivalence_toDescentData 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows	CategoryTheory.Functor.IsEquivalence CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str DescentData DescentData.instCategory toDescentData	—	isStackFor_ofArrows_iff IsStackFor_generate_iff isStackFor CategoryTheory.Sieve.generate_sieve
isStackFor 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.generate	IsStackFor	—	isStackFor'
isStackFor' 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	IsStackFor CategoryTheory.Sieve.arrows	—	isStackFor_iff isPrestackFor' IsStack.toIsPrestack CategoryTheory.Functor.FullyFaithful.full CategoryTheory.Functor.FullyFaithful.faithful IsStack.essSurj_of_sieve

CategoryTheory.Pseudofunctor.IsStack

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essSurj_of_sieve 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	CategoryTheory.Functor.EssSurj CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Presieve.category CategoryTheory.Sieve.arrows CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData.instCategory CategoryTheory.Pseudofunctor.toDescentData	—	—
of_isStackFor 📖	mathematical	CategoryTheory.Pseudofunctor.IsStackFor CategoryTheory.Sieve.arrows	CategoryTheory.Pseudofunctor.IsStack	—	CategoryTheory.Pseudofunctor.IsPrestack.of_isPrestackFor CategoryTheory.Pseudofunctor.IsStackFor.isPrestackFor CategoryTheory.Pseudofunctor.isStackFor_iff CategoryTheory.Functor.IsEquivalence.essSurj
toIsPrestack 📖	mathematical	—	CategoryTheory.Pseudofunctor.IsPrestack	—	—

---

← Back to Index