Documentation Verification Report

Grothendieck

📁 Source: Mathlib/CategoryTheory/Bicategory/Grothendieck.lean

Statistics

Metric	Count
Definitions `CoGrothendieck`, `base`, `fiber`, `base`, `category`, `categoryStruct`, `fiber`, `forget`, `instInhabitedHom`, `map`, `mapCompIso`, `mapIdIso`, `«term∫ᶜ_»`, `base`, `fiber`, `base`, `category`, `categoryStruct`, `fiber`, `forget`, `instInhabitedHom`, `map`, `mapCompIso`, `mapIdIso`, `«term∫_»`	25
Theorems `ext`, `ext_iff`, `categoryStruct_comp_base`, `categoryStruct_comp_fiber`, `categoryStruct_id_base`, `categoryStruct_id_fiber`, `ext`, `ext_iff`, `forget_map`, `forget_obj`, `map_comp_eq`, `map_comp_forget`, `map_id_eq`, `map_id_map`, `map_map_base`, `map_map_fiber`, `map_obj_base`, `map_obj_fiber`, `ext`, `ext_iff`, `categoryStruct_comp_base`, `categoryStruct_comp_fiber`, `categoryStruct_id_base`, `categoryStruct_id_fiber`, `ext`, `ext_iff`, `forget_map`, `forget_obj`, `map_comp_eq`, `map_comp_forget`, `map_id_eq`, `map_id_map`, `map_map_base`, `map_map_fiber`, `map_obj_base`, `map_obj_fiber`	36
Total	61

CategoryTheory.Pseudofunctor

Definitions

Name	Category	Theorems
`CoGrothendieck` 📖	CompData	30 math math: `CoGrothendieck.categoryStruct_id_base`, `CoGrothendieck.categoryStruct_id_fiber`, `CoGrothendieck.map_comp_eq`, `CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CoGrothendieck.map_map_base`, `CoGrothendieck.map_map_fiber`, `CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CoGrothendieck.ι_map_base`, `CoGrothendieck.map_obj_fiber`, `CoGrothendieck.Hom.congr`, `CoGrothendieck.categoryStruct_comp_base`, `CoGrothendieck.ι_obj_fiber`, `CoGrothendieck.ι_map_fiber`, `CoGrothendieck.isStronglyCartesian_homCartesianLift`, `CoGrothendieck.isHomLift_cartesianLift`, `CoGrothendieck.instIsFiberedForget`, `CoGrothendieck.forget_obj`, `CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CoGrothendieck.ι_obj_base`, `CoGrothendieck.map_comp_forget`, `CoGrothendieck.comp_const`, `CoGrothendieck.map_id_eq`, `CoGrothendieck.map_obj_base`, `CoGrothendieck.compIso_inv_app`, `CoGrothendieck.categoryStruct_comp_fiber`, `CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CoGrothendieck.map_id_map`, `CoGrothendieck.forget_map`, `CoGrothendieck.compIso_hom_app`, `CoGrothendieck.isHomLift_homCartesianLift`

CategoryTheory.Pseudofunctor.CoGrothendieck

Definitions

Name	Category	Theorems
`base` 📖	CompOp	15 math math: `categoryStruct_id_base`, `categoryStruct_id_fiber`, `map_map_base`, `map_map_fiber`, `map_obj_fiber`, `Hom.congr`, `categoryStruct_comp_base`, `ext_iff`, `ι_map_fiber`, `forget_obj`, `ι_obj_base`, `map_obj_base`, `categoryStruct_comp_fiber`, `Hom.ext_iff`, `isHomLift_homCartesianLift`
`category` 📖	CompOp	25 math math: `map_comp_eq`, `instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `map_map_base`, `map_map_fiber`, `instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `ι_map_base`, `map_obj_fiber`, `ι_obj_fiber`, `ι_map_fiber`, `isStronglyCartesian_homCartesianLift`, `isHomLift_cartesianLift`, `instIsFiberedForget`, `forget_obj`, `instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `ι_obj_base`, `map_comp_forget`, `comp_const`, `map_id_eq`, `map_obj_base`, `compIso_inv_app`, `instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `map_id_map`, `forget_map`, `compIso_hom_app`, `isHomLift_homCartesianLift`
`categoryStruct` 📖	CompOp	5 math math: `categoryStruct_id_base`, `categoryStruct_id_fiber`, `Hom.congr`, `categoryStruct_comp_base`, `categoryStruct_comp_fiber`
`fiber` 📖	CompOp	10 math math: `categoryStruct_id_fiber`, `map_map_base`, `map_map_fiber`, `map_obj_fiber`, `Hom.congr`, `ext_iff`, `ι_obj_fiber`, `ι_map_fiber`, `categoryStruct_comp_fiber`, `Hom.ext_iff`
`forget` 📖	CompOp	14 math math: `instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `isStronglyCartesian_homCartesianLift`, `isHomLift_cartesianLift`, `instIsFiberedForget`, `forget_obj`, `instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `map_comp_forget`, `comp_const`, `compIso_inv_app`, `instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `forget_map`, `compIso_hom_app`, `isHomLift_homCartesianLift`
`instInhabitedHom` 📖	CompOp	—
`map` 📖	CompOp	8 math math: `map_comp_eq`, `map_map_base`, `map_map_fiber`, `map_obj_fiber`, `map_comp_forget`, `map_id_eq`, `map_obj_base`, `map_id_map`
`mapCompIso` 📖	CompOp	—
`mapIdIso` 📖	CompOp	—
`«term∫ᶜ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`categoryStruct_comp_base` 📖	mathematical	—	`Hom.base` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Pseudofunctor.CoGrothendieck` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `base`	—	—
`categoryStruct_comp_fiber` 📖	mathematical	—	`Hom.fiber` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Pseudofunctor.CoGrothendieck` `categoryStruct` `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` `base` `CategoryTheory.Cat.str` `fiber` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `Hom.base` `CategoryTheory.LocallyDiscrete.categoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Iso.inv` `CategoryTheory.Pseudofunctor.mapComp`	—	—
`categoryStruct_id_base` 📖	mathematical	—	`Hom.base` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor.CoGrothendieck` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `base`	—	—
`categoryStruct_id_fiber` 📖	mathematical	—	`Hom.fiber` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor.CoGrothendieck` `categoryStruct` `CategoryTheory.NatTrans.app` `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` `base` `CategoryTheory.Cat.str` `CategoryTheory.Functor.id` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Iso.inv` `CategoryTheory.Pseudofunctor.mapId` `fiber`	—	—
`ext` 📖	—	`base` `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` `fiber`	—	—	—
`ext_iff` 📖	mathematical	—	`base` `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` `fiber`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `Hom.base`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `base`	—	—
`map_comp_eq` 📖	mathematical	—	`map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Pseudofunctor` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category`	—	`CategoryTheory.Functor.ext_of_iso` `CategoryTheory.Bicategory.Strict.associator_eqToIso` `CategoryTheory.Cat.bicategory.strict` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`map_comp_forget` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `map` `forget`	—	—
`map_id_eq` 📖	mathematical	—	`map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category`	—	`CategoryTheory.Functor.ext_of_iso` `CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso` `CategoryTheory.Cat.bicategory.strict` `CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`map_id_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct`	—	`Hom.ext` `CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso` `CategoryTheory.Cat.bicategory.strict` `CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`map_map_base` 📖	mathematical	—	`Hom.base` `base` `CategoryTheory.Functor.obj` `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` `CategoryTheory.Pseudofunctor.StrongTrans.app` `fiber` `CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `map`	—	—
`map_map_fiber` 📖	mathematical	—	`Hom.fiber` `base` `CategoryTheory.Functor.obj` `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` `CategoryTheory.Pseudofunctor.StrongTrans.app` `fiber` `CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `map` `CategoryTheory.CategoryStruct.comp` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `Hom.base` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.StrongTrans.naturality`	—	—
`map_obj_base` 📖	mathematical	—	`base` `CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `map`	—	—
`map_obj_fiber` 📖	mathematical	—	`fiber` `CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `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` `base` `CategoryTheory.Cat.str` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Pseudofunctor.StrongTrans.app`	—	—

CategoryTheory.Pseudofunctor.CoGrothendieck.Hom

Definitions

Name	Category	Theorems
`base` 📖	CompOp	9 math math: `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_base`, `CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base`, `CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber`, `CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_base`, `congr`, `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_base`, `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `CategoryTheory.Pseudofunctor.CoGrothendieck.forget_map`, `ext_iff`
`fiber` 📖	CompOp	6 math math: `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber`, `CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber`, `congr`, `CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber`, `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`base` `fiber` `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.Pseudofunctor.CoGrothendieck.base` `CategoryTheory.Cat.str` `CategoryTheory.Pseudofunctor.CoGrothendieck.fiber` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.eqToHom`	—	—	`CategoryTheory.Category.comp_id`
`ext_iff` 📖	mathematical	—	`fiber` `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.Pseudofunctor.CoGrothendieck.base` `CategoryTheory.Cat.str` `CategoryTheory.Pseudofunctor.CoGrothendieck.fiber` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `base` `CategoryTheory.eqToHom`	—	`CategoryTheory.eqToHom_naturality` `CategoryTheory.Category.id_comp` `ext`

CategoryTheory.Pseudofunctor.Grothendieck

Definitions

Name	Category	Theorems
`base` 📖	CompOp	12 math math: `ext_iff`, `categoryStruct_id_fiber`, `map_obj_fiber`, `categoryStruct_id_base`, `Hom.ext_iff`, `Hom.congr`, `map_map_fiber`, `categoryStruct_comp_base`, `forget_obj`, `map_obj_base`, `categoryStruct_comp_fiber`, `map_map_base`
`category` 📖	CompOp	10 math math: `map_id_eq`, `map_id_map`, `map_obj_fiber`, `forget_map`, `map_comp_forget`, `map_comp_eq`, `map_map_fiber`, `forget_obj`, `map_obj_base`, `map_map_base`
`categoryStruct` 📖	CompOp	5 math math: `categoryStruct_id_fiber`, `categoryStruct_id_base`, `Hom.congr`, `categoryStruct_comp_base`, `categoryStruct_comp_fiber`
`fiber` 📖	CompOp	8 math math: `ext_iff`, `categoryStruct_id_fiber`, `map_obj_fiber`, `Hom.ext_iff`, `Hom.congr`, `map_map_fiber`, `categoryStruct_comp_fiber`, `map_map_base`
`forget` 📖	CompOp	3 math math: `forget_map`, `map_comp_forget`, `forget_obj`
`instInhabitedHom` 📖	CompOp	—
`map` 📖	CompOp	8 math math: `map_id_eq`, `map_id_map`, `map_obj_fiber`, `map_comp_forget`, `map_comp_eq`, `map_map_fiber`, `map_obj_base`, `map_map_base`
`mapCompIso` 📖	CompOp	—
`mapIdIso` 📖	CompOp	—
`«term∫_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`categoryStruct_comp_base` 📖	mathematical	—	`Hom.base` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Pseudofunctor.Grothendieck` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `base`	—	—
`categoryStruct_comp_fiber` 📖	mathematical	—	`Hom.fiber` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Pseudofunctor.Grothendieck` `categoryStruct` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `base` `CategoryTheory.Cat.str` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `CategoryTheory.LocallyDiscrete.categoryStruct` `Quiver.Hom.toLoc` `Hom.base` `fiber` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.mapComp` `CategoryTheory.Functor.map`	—	—
`categoryStruct_id_base` 📖	mathematical	—	`Hom.base` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor.Grothendieck` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `base`	—	—
`categoryStruct_id_fiber` 📖	mathematical	—	`Hom.fiber` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor.Grothendieck` `categoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `base` `CategoryTheory.Cat.str` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `CategoryTheory.Functor.id` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.mapId` `fiber`	—	—
`ext` 📖	—	`base` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `fiber`	—	—	—
`ext_iff` 📖	mathematical	—	`base` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `fiber`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.Grothendieck` `category` `forget` `Hom.base`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.Grothendieck` `category` `forget` `base`	—	—
`map_comp_eq` 📖	mathematical	—	`map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Pseudofunctor` `CategoryTheory.LocallyDiscrete` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Pseudofunctor.Grothendieck` `category`	—	`CategoryTheory.Functor.ext_of_iso` `CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv` `CategoryTheory.Bicategory.Strict.associator_eqToIso` `CategoryTheory.Cat.bicategory.strict` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc`
`map_comp_forget` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.Pseudofunctor.Grothendieck` `category` `map` `forget`	—	—
`map_id_eq` 📖	mathematical	—	`map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor` `CategoryTheory.LocallyDiscrete` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Pseudofunctor.Grothendieck` `category`	—	`CategoryTheory.Functor.ext_of_iso` `CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso` `CategoryTheory.Cat.bicategory.strict` `CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso` `CategoryTheory.Category.id_comp`
`map_id_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.Grothendieck` `category` `map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor` `CategoryTheory.LocallyDiscrete` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct`	—	`Hom.ext` `CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso` `CategoryTheory.Cat.bicategory.strict` `CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso` `CategoryTheory.Category.id_comp`
`map_map_base` 📖	mathematical	—	`Hom.base` `base` `CategoryTheory.Functor.obj` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `CategoryTheory.Cat.str` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Pseudofunctor.StrongTrans.app` `fiber` `CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.Grothendieck` `category` `map`	—	—
`map_map_fiber` 📖	mathematical	—	`Hom.fiber` `base` `CategoryTheory.Functor.obj` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `CategoryTheory.Cat.str` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Pseudofunctor.StrongTrans.app` `fiber` `CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.Grothendieck` `category` `map` `CategoryTheory.CategoryStruct.comp` `Prefunctor.map` `Quiver.Hom.toLoc` `Hom.base` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Iso.inv` `CategoryTheory.Pseudofunctor.StrongTrans.naturality`	—	—
`map_obj_base` 📖	mathematical	—	`base` `CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.Grothendieck` `category` `map`	—	—
`map_obj_fiber` 📖	mathematical	—	`fiber` `CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.Grothendieck` `category` `map` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `base` `CategoryTheory.Cat.str` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Pseudofunctor.StrongTrans.app`	—	—

CategoryTheory.Pseudofunctor.Grothendieck.Hom

Definitions

Name	Category	Theorems
`base` 📖	CompOp	8 math math: `CategoryTheory.Pseudofunctor.Grothendieck.forget_map`, `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_base`, `ext_iff`, `congr`, `CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber`, `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_base`, `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`, `CategoryTheory.Pseudofunctor.Grothendieck.map_map_base`
`fiber` 📖	CompOp	5 math math: `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber`, `ext_iff`, `congr`, `CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber`, `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`base` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `CategoryTheory.Pseudofunctor.Grothendieck.base` `CategoryTheory.Cat.str` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.Pseudofunctor.Grothendieck.fiber` `CategoryTheory.eqToHom` `fiber`	—	—	`CategoryTheory.Category.id_comp`
`ext_iff` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `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.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `CategoryTheory.Pseudofunctor.Grothendieck.base` `CategoryTheory.Cat.str` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `Quiver.Hom.toLoc` `base` `CategoryTheory.Pseudofunctor.Grothendieck.fiber` `CategoryTheory.eqToHom` `fiber`	—	`CategoryTheory.Category.id_comp` `ext`

---

← Back to Index