PseudofunctorSheafOver

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

Statistics

Metric	Count
Definitions pseudofunctorOver	1
Theorems pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app, pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_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_mapComp_inv_toNatTrans_app_hom_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app, pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app, pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app, pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category 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.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory 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.Over.mapComp	—	CategoryTheory.Category.comp_id
pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category 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.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory 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.Over.mapComp	—	CategoryTheory.Category.id_comp
pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory 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.Over.mapId	—	CategoryTheory.Category.comp_id
pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.id CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory 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.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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.toCatHom overMapPullback Quiver.Hom.unop CategoryTheory.Discrete.as CategoryTheory.Bicategory.instIsLocallyDiscreteLocallyDiscrete	—	—
pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Sheaf over CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp CategoryTheory.sheafToPresheaf CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Over.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.op_comp_isSheaf instIsContinuousOverMapOver CategoryTheory.Functor.map 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_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category 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_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category 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_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.comp 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_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop CategoryTheory.LocallyDiscrete.as CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.id 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