Documentation Verification Report

Grothendieck

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

Statistics

Metric	Count
Definitions `cartesianLift`, `compIso`, `domainCartesianLift`, `homCartesianLift`, `instHasFibersForget`, `ι`	6
Theorems `compIso_hom_app`, `compIso_inv_app`, `comp_const`, `instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `instIsFiberedForget`, `isHomLift_cartesianLift`, `isHomLift_homCartesianLift`, `isStronglyCartesian_homCartesianLift`, `ι_map_base`, `ι_map_fiber`, `ι_obj_base`, `ι_obj_fiber`	15
Total	21

CategoryTheory.Pseudofunctor.CoGrothendieck

Definitions

Name	Category	Theorems
`cartesianLift` 📖	CompOp	2 math math: `isStronglyCartesian_homCartesianLift`, `isHomLift_cartesianLift`
`compIso` 📖	CompOp	2 math math: `compIso_inv_app`, `compIso_hom_app`
`domainCartesianLift` 📖	CompOp	3 math math: `isStronglyCartesian_homCartesianLift`, `isHomLift_cartesianLift`, `isHomLift_homCartesianLift`
`homCartesianLift` 📖	CompOp	1 math math: `isHomLift_homCartesianLift`
`instHasFibersForget` 📖	CompOp	—
`ι` 📖	CompOp	11 math math: `instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `ι_map_base`, `ι_obj_fiber`, `ι_map_fiber`, `instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `ι_obj_base`, `comp_const`, `compIso_inv_app`, `instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `compIso_hom_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compIso_hom_app` 📖	mathematical	—	`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` `CategoryTheory.Cat.str` `CategoryTheory.Functor.comp` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `ι` `forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Iso.hom` `compIso` `CategoryTheory.CategoryStruct.id`	—	—
`compIso_inv_app` 📖	mathematical	—	`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` `CategoryTheory.Cat.str` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Functor.comp` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `ι` `forget` `CategoryTheory.Iso.inv` `compIso` `CategoryTheory.CategoryStruct.id`	—	—
`comp_const` 📖	mathematical	—	`CategoryTheory.Functor.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.Pseudofunctor.CoGrothendieck` `category` `ι` `forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const`	—	`CategoryTheory.Functor.ext_of_iso`
`instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `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.Functor.Fiber` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `CategoryTheory.Cat.str` `CategoryTheory.Functor.Fiber.fiberCategory` `CategoryTheory.Functor.Fiber.inducedFunctor` `ι` `comp_const`	—	`CategoryTheory.Functor.essSurj_of_surj` `comp_const` `ext`
`instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `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.Fiber` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `CategoryTheory.Functor.Fiber.fiberCategory` `CategoryTheory.Functor.Fiber.inducedFunctor` `ι` `comp_const`	—	`comp_const` `CategoryTheory.Functor.congr_map` `Hom.ext_iff` `CategoryTheory.Category.comp_id` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.NatIso.inv_app_isIso`
`instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `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.Fiber` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `CategoryTheory.Functor.Fiber.fiberCategory` `CategoryTheory.Functor.Fiber.inducedFunctor` `ι` `comp_const`	—	`comp_const` `CategoryTheory.IsHomLift.domain_eq` `CategoryTheory.Functor.Fiber.instIsHomLiftIdMapFiberInclusion` `CategoryTheory.IsHomLift.codomain_eq` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.IsHomLift.fac` `CategoryTheory.Functor.Fiber.hom_ext` `Hom.ext` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id`
`instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `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.Fiber` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `CategoryTheory.Functor.Fiber.fiberCategory` `CategoryTheory.Functor.Fiber.inducedFunctor` `ι` `comp_const`	—	`comp_const` `instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor` `instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor` `instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`
`instIsFiberedForget` 📖	mathematical	—	`CategoryTheory.Functor.IsFibered` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget`	—	`CategoryTheory.Functor.IsFibered.of_exists_isStronglyCartesian` `isStronglyCartesian_homCartesianLift`
`isHomLift_cartesianLift` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `domainCartesianLift` `cartesianLift`	—	`CategoryTheory.IsHomLift.map`
`isHomLift_homCartesianLift` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `base` `domainCartesianLift` `homCartesianLift`	—	`CategoryTheory.IsHomLift.map`
`isStronglyCartesian_homCartesianLift` 📖	mathematical	—	`CategoryTheory.Functor.IsStronglyCartesian` `CategoryTheory.Pseudofunctor.CoGrothendieck` `category` `forget` `domainCartesianLift` `cartesianLift`	—	`isHomLift_cartesianLift` `isHomLift_homCartesianLift` `Hom.ext` `CategoryTheory.IsHomLift.domain_eq` `CategoryTheory.IsHomLift.codomain_eq` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.IsHomLift.fac` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Iso.inv_hom_id`
`ι_map_base` 📖	mathematical	—	`Hom.base` `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.Pseudofunctor.CoGrothendieck` `category` `ι` `CategoryTheory.CategoryStruct.id`	—	—
`ι_map_fiber` 📖	mathematical	—	`Hom.fiber` `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.Pseudofunctor.CoGrothendieck` `category` `ι` `CategoryTheory.CategoryStruct.comp` `base` `fiber` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Iso.inv` `CategoryTheory.Pseudofunctor.mapId`	—	—
`ι_obj_base` 📖	mathematical	—	`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.Pseudofunctor.CoGrothendieck` `category` `ι`	—	—
`ι_obj_fiber` 📖	mathematical	—	`fiber` `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.Pseudofunctor.CoGrothendieck` `category` `ι`	—	—

---

← Back to Index