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_val	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', presheafHomObjHomEquiv_symm_apply, isPrestackFor_iff_isSheafFor', sheafHom_val
presheafHomObjHomEquiv 📖	CompOp	3 math math: DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, presheafHomObjHomEquiv_apply, presheafHomObjHomEquiv_symm_apply
sheafHom 📖	CompOp	1 math math: sheafHom_val

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.Cat.Hom.toFunctor Prefunctor.map CategoryTheory.LocallyDiscrete.categoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor.id 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.Cat.Hom.toFunctor Prefunctor.map CategoryTheory.LocallyDiscrete.categoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor.id 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_val 📖	mathematical	—	CategoryTheory.Sheaf.val CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.GrothendieckTopology.over CategoryTheory.types 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	6 math math: CategoryTheory.Pseudofunctor.presheafHom_map, CategoryTheory.Pseudofunctor.DescentData.pullHom_hom, pullHom_pullHom, pullHom_id, map_eq_pullHom_assoc, map_eq_pullHom

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.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.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.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.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.Pseudofunctor.mapComp'_comp_id_hom_app CategoryTheory.locallyDiscreteBicategory.strict CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Cat.Hom₂.comp_app CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.id_comp
pullHom_pullHom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullHom	—	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