PseudofunctorSheafOver

📁 Source: Mathlib/CategoryTheory/Sites/PseudofunctorSheafOver.lean

Statistics

Metric	Count
Definitions pseudofunctorOver	1
Theorems pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α	11
Total	12

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
pseudofunctorOver 📖	CompOp	11 math math: pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, pseudofunctorOver_mapId_hom_toNatTrans_app_val_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.Functor.comp instIsContinuousOverMapOver CategoryTheory.Sheaf.Hom.val overMapPullback CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat.bicategory pseudofunctorOver CategoryTheory.Functor.map Opposite.op Quiver.Hom.op CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Over.mapComp	—	CategoryTheory.Category.comp_id
pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.comp CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Discrete.as Quiver.Hom instIsContinuousOverMapOver CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf.Hom.val CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor overMapPullback CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat.bicategory pseudofunctorOver CategoryTheory.Functor.map Opposite.op Quiver.Hom.op CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Over.mapComp	—	CategoryTheory.Category.id_comp
pseudofunctorOver_mapId_hom_toNatTrans_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.Sheaf.Hom.val overMapPullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat.bicategory pseudofunctorOver CategoryTheory.Functor.map Opposite.op Quiver.Hom.op CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Over.mapId	—	CategoryTheory.Category.comp_id
pseudofunctorOver_mapId_inv_toNatTrans_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.id CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.Hom.val CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str overMapPullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat.bicategory pseudofunctorOver CategoryTheory.Functor.map Opposite.op Quiver.Hom.op CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Over.mapId	—	CategoryTheory.Category.id_comp
pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ 📖	mathematical	—	CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorOver CategoryTheory.eqToHom CategoryTheory.Cat.of CategoryTheory.Sheaf CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.instCategoryOver over CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.toCatHom overMapPullback Quiver.Hom.unop CategoryTheory.Discrete.as CategoryTheory.Bicategory.instIsLocallyDiscreteLocallyDiscrete	—	—
pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Over.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.Sheaf.val over CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.comp CategoryTheory.Functor.op_comp_isSheaf instIsContinuousOverMapOver CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of Prefunctor.map CategoryTheory.LocallyDiscrete CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorOver Opposite.op	—	CategoryTheory.Functor.op_comp_isSheaf instIsContinuousOverMapOver
pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of Prefunctor.map CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorOver Opposite.op CategoryTheory.Over.map Quiver.Hom.unop CategoryTheory.Discrete.as Quiver.Hom.op	—	—
pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of Prefunctor.map CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorOver Opposite.op CategoryTheory.Over.map Quiver.Hom.unop CategoryTheory.Discrete.as	—	—
pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Sheaf.Hom.val CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Bundled.str CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorOver CategoryTheory.Functor.obj	—	—
pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Sheaf.Hom.val CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Bundled.str CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorOver CategoryTheory.Functor.obj	—	—
pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α 📖	mathematical	—	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 pseudofunctorOver CategoryTheory.Sheaf CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.instCategoryOver over	—	—

---

← Back to Index