IsPrestack

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

Statistics

Metric	Count
Definitions IsPrestack, pullHom, overMapCompPresheafHomIso, presheafHom, presheafHomObjHomEquiv, sheafHom	6
Theorems isSheaf, map_eq_pullHom, map_eq_pullHom_assoc, pullHom_id, pullHom_pullHom, presheafHomObjHomEquiv_apply, presheafHomObjHomEquiv_symm_apply, presheafHom_map, presheafHom_obj, sheafHom_obj	10
Total	16

CategoryTheory.Pseudofunctor

Definitions

Name	Category	Theorems
IsPrestack 📖	CompData	3 math math: IsPrestack.of_isPrestackFor, IsPrestack.of_precoverage, IsStack.toIsPrestack
overMapCompPresheafHomIso 📖	CompOp	—
presheafHom 📖	CompOp	11 math math: DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, presheafHom_obj, isPrestackFor_iff_isSheafFor, bijective_toDescentData_map_iff, presheafHom_map, IsPrestack.isSheaf, presheafHomObjHomEquiv_apply, IsPrestackFor.isSheafFor', sheafHom_obj, presheafHomObjHomEquiv_symm_apply, isPrestackFor_iff_isSheafFor'
presheafHomObjHomEquiv 📖	CompOp	3 math math: DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, presheafHomObjHomEquiv_apply, presheafHomObjHomEquiv_symm_apply
sheafHom 📖	CompOp	1 math math: sheafHom_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presheafHomObjHomEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom 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 CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.types presheafHom CategoryTheory.CategoryStruct.id EquivLike.toFunLike Equiv.instEquivLike presheafHomObjHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.id Opposite.unop CategoryTheory.Comma.left CategoryTheory.Cat.Hom.toFunctor Prefunctor.map CategoryTheory.LocallyDiscrete.categoryStruct CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory mapId CategoryTheory.Iso.inv	—	—
presheafHomObjHomEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.types presheafHom Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor CategoryTheory.Cat.str EquivLike.toFunLike Equiv.instEquivLike Equiv.symm presheafHomObjHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.id Opposite.unop CategoryTheory.Comma.left CategoryTheory.Cat.Hom.toFunctor Prefunctor.map CategoryTheory.LocallyDiscrete.categoryStruct CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory mapId CategoryTheory.Iso.hom	—	—
presheafHom_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.types presheafHom LocallyDiscreteOpToCat.pullHom CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.id Opposite.unop CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
presheafHom_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.types presheafHom Quiver.Hom CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Cat.str CategoryTheory.Comma.right CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc Quiver.Hom.op CategoryTheory.Comma.hom	—	—
sheafHom_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.over sheafHom presheafHom	—	—

CategoryTheory.Pseudofunctor.IsPrestack

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.types CategoryTheory.GrothendieckTopology.over CategoryTheory.Pseudofunctor.presheafHom	—	—

CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat

Definitions

Name	Category	Theorems
pullHom 📖	CompOp	16 math math: CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom', CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.presheafHom_map, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData.pullHom_hom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, pullHom_pullHom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom, pullHom_id, map_eq_pullHom_assoc, map_eq_pullHom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq_pullHom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.map 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.Cat.str CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.mapComp' pullHom CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Cat.Hom₂.comp_app CategoryTheory.Category.id_comp
map_eq_pullHom_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp 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.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.mapComp' pullHom CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_eq_pullHom
pullHom_id 📖	mathematical	—	pullHom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.locallyDiscreteBicategory.strict CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app CategoryTheory.Category.id_comp CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app CategoryTheory.Category.comp_id CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Cat.Hom₂.comp_app CategoryTheory.Iso.inv_hom_id
pullHom_pullHom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullHom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Functor.map_comp_assoc CategoryTheory.locallyDiscreteBicategory.strict CategoryTheory.Category.assoc CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Cat.Hom₂.comp_app CategoryTheory.Iso.hom_inv_id CategoryTheory.Cat.Hom₂.id_app CategoryTheory.Category.id_comp

---

← Back to Index