Documentation Verification Report

BasedCategory

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

Statistics

Metric	Count
Definitions `BasedCategory`, `bicategory`, `category`, `instCategory`, `obj`, `ofFunctor`, `p`, `whiskerLeft`, `whiskerRight`, `BasedFunctor`, `comp`, `id`, `toFunctor`, `«term_⋙_»`, `«term𝟭»`, `id`, `mkNatIso`, `BasedNatTrans`, `comp`, `forgetful`, `homCategory`, `id`, `toNatTrans`, `instCategoryObj`, `«term_⥤ᵇ_»`	25
Theorems `comp_def`, `id_def`, `instStrict`, `whiskerLeft_toNatTrans`, `whiskerRight_toNatTrans`, `comp_assoc`, `comp_id`, `comp_toFunctor`, `id_comp`, `id_toFunctor`, `instIsHomLiftObjPIdObj`, `isHomLift_iff`, `isHomLift_map`, `preserves_isHomLift`, `w`, `w_obj`, `id_hom`, `id_inv`, `isIso_of_toNatTrans_isIso`, `app_isHomLift`, `comp_toNatTrans`, `ext`, `ext_iff`, `forgetful_map`, `forgetful_obj`, `ext`, `ext_iff`, `homCategory_comp`, `homCategory_id`, `id_toNatTrans`, `instIsIsoFunctorObjOfBasedFunctor`, `instReflectsIsomorphismsBasedFunctorFunctorObjForgetful`, `isHomLift`, `isHomLift'`	34
Total	59

CategoryTheory

Definitions

Name	Category	Theorems
`BasedCategory` 📖	CompData	3 math math: `BasedCategory.comp_def`, `BasedCategory.instStrict`, `BasedCategory.id_def`
`BasedFunctor` 📖	CompData	8 math math: `BasedNatIso.id_hom`, `BasedNatIso.isIso_of_toNatTrans_isIso`, `BasedNatTrans.forgetful_map`, `BasedNatIso.id_inv`, `BasedNatTrans.homCategory_comp`, `BasedNatTrans.instReflectsIsomorphismsBasedFunctorFunctorObjForgetful`, `BasedNatTrans.homCategory_id`, `BasedNatTrans.forgetful_obj`
`BasedNatTrans` 📖	CompData	—
`instCategoryObj` 📖	CompOp	18 math math: `BasedNatTrans.id_toNatTrans`, `BasedNatTrans.isHomLift'`, `BasedCategory.whiskerLeft_toNatTrans`, `BasedCategory.whiskerRight_toNatTrans`, `BasedFunctor.w_obj`, `BasedNatTrans.forgetful_map`, `BasedNatTrans.comp_toNatTrans`, `BasedFunctor.id_toFunctor`, `BasedFunctor.w`, `BasedFunctor.instIsHomLiftObjPIdObj`, `BasedFunctor.isHomLift_iff`, `BasedFunctor.preserves_isHomLift`, `BasedNatTrans.instIsIsoFunctorObjOfBasedFunctor`, `BasedNatTrans.instReflectsIsomorphismsBasedFunctorFunctorObjForgetful`, `BasedFunctor.comp_toFunctor`, `BasedNatTrans.app_isHomLift`, `BasedNatTrans.isHomLift`, `BasedNatTrans.forgetful_obj`
`«term_⥤ᵇ_»` 📖	CompOp	—

CategoryTheory.BasedCategory

Definitions

Name	Category	Theorems
`bicategory` 📖	CompOp	1 math math: `instStrict`
`category` 📖	CompOp	7 math math: `CategoryTheory.BasedNatTrans.isHomLift'`, `CategoryTheory.BasedFunctor.isHomLift_map`, `CategoryTheory.BasedFunctor.w_obj`, `CategoryTheory.BasedFunctor.instIsHomLiftObjPIdObj`, `CategoryTheory.BasedFunctor.isHomLift_iff`, `CategoryTheory.BasedFunctor.preserves_isHomLift`, `CategoryTheory.BasedNatTrans.app_isHomLift`
`instCategory` 📖	CompOp	2 math math: `comp_def`, `id_def`
`obj` 📖	CompOp	18 math math: `CategoryTheory.BasedNatTrans.id_toNatTrans`, `CategoryTheory.BasedNatTrans.isHomLift'`, `whiskerLeft_toNatTrans`, `whiskerRight_toNatTrans`, `CategoryTheory.BasedFunctor.isHomLift_map`, `CategoryTheory.BasedFunctor.w_obj`, `CategoryTheory.BasedNatTrans.forgetful_map`, `CategoryTheory.BasedNatTrans.comp_toNatTrans`, `CategoryTheory.BasedFunctor.id_toFunctor`, `CategoryTheory.BasedFunctor.w`, `CategoryTheory.BasedFunctor.instIsHomLiftObjPIdObj`, `CategoryTheory.BasedFunctor.isHomLift_iff`, `CategoryTheory.BasedFunctor.preserves_isHomLift`, `CategoryTheory.BasedNatTrans.instIsIsoFunctorObjOfBasedFunctor`, `CategoryTheory.BasedNatTrans.instReflectsIsomorphismsBasedFunctorFunctorObjForgetful`, `CategoryTheory.BasedFunctor.comp_toFunctor`, `CategoryTheory.BasedNatTrans.app_isHomLift`, `CategoryTheory.BasedNatTrans.forgetful_obj`
`ofFunctor` 📖	CompOp	—
`p` 📖	CompOp	8 math math: `CategoryTheory.BasedNatTrans.isHomLift'`, `CategoryTheory.BasedFunctor.isHomLift_map`, `CategoryTheory.BasedFunctor.w_obj`, `CategoryTheory.BasedFunctor.w`, `CategoryTheory.BasedFunctor.instIsHomLiftObjPIdObj`, `CategoryTheory.BasedFunctor.isHomLift_iff`, `CategoryTheory.BasedFunctor.preserves_isHomLift`, `CategoryTheory.BasedNatTrans.app_isHomLift`
`whiskerLeft` 📖	CompOp	1 math math: `whiskerLeft_toNatTrans`
`whiskerRight` 📖	CompOp	1 math math: `whiskerRight_toNatTrans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_def` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.BasedCategory` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.BasedFunctor.comp`	—	—
`id_def` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `CategoryTheory.BasedCategory` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.BasedFunctor.id`	—	—
`instStrict` 📖	mathematical	—	`CategoryTheory.Bicategory.Strict` `CategoryTheory.BasedCategory` `bicategory`	—	—
`whiskerLeft_toNatTrans` 📖	mathematical	—	`CategoryTheory.BasedNatTrans.toNatTrans` `CategoryTheory.BasedFunctor.comp` `whiskerLeft` `CategoryTheory.Functor.whiskerLeft` `obj` `CategoryTheory.instCategoryObj` `CategoryTheory.BasedFunctor.toFunctor`	—	—
`whiskerRight_toNatTrans` 📖	mathematical	—	`CategoryTheory.BasedNatTrans.toNatTrans` `CategoryTheory.BasedFunctor.comp` `whiskerRight` `CategoryTheory.Functor.whiskerRight` `obj` `CategoryTheory.instCategoryObj` `CategoryTheory.BasedFunctor.toFunctor`	—	—

CategoryTheory.BasedFunctor

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	7 math math: `CategoryTheory.BasedCategory.comp_def`, `CategoryTheory.BasedCategory.whiskerLeft_toNatTrans`, `comp_id`, `CategoryTheory.BasedCategory.whiskerRight_toNatTrans`, `comp_assoc`, `id_comp`, `comp_toFunctor`
`id` 📖	CompOp	4 math math: `comp_id`, `id_comp`, `id_toFunctor`, `CategoryTheory.BasedCategory.id_def`
`toFunctor` 📖	CompOp	16 math math: `CategoryTheory.BasedNatTrans.id_toNatTrans`, `CategoryTheory.BasedNatTrans.isHomLift'`, `CategoryTheory.BasedCategory.whiskerLeft_toNatTrans`, `CategoryTheory.BasedCategory.whiskerRight_toNatTrans`, `w_obj`, `CategoryTheory.BasedNatTrans.comp_toNatTrans`, `id_toFunctor`, `w`, `instIsHomLiftObjPIdObj`, `isHomLift_iff`, `preserves_isHomLift`, `CategoryTheory.BasedNatTrans.instIsIsoFunctorObjOfBasedFunctor`, `comp_toFunctor`, `CategoryTheory.BasedNatTrans.app_isHomLift`, `CategoryTheory.BasedNatTrans.isHomLift`, `CategoryTheory.BasedNatTrans.forgetful_obj`
`«term_⋙_»` 📖	CompOp	—
`«term𝟭»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`comp_toFunctor` 📖	mathematical	—	`toFunctor` `comp` `CategoryTheory.Functor.comp` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`id_toFunctor` 📖	mathematical	—	`toFunctor` `id` `CategoryTheory.Functor.id` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj`	—	—
`instIsHomLiftObjPIdObj` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.BasedCategory.obj` `CategoryTheory.BasedCategory.category` `CategoryTheory.BasedCategory.p` `CategoryTheory.Functor.obj` `CategoryTheory.instCategoryObj` `toFunctor` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.IsHomLift.id` `w_obj`
`isHomLift_iff` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.BasedCategory.obj` `CategoryTheory.BasedCategory.category` `CategoryTheory.BasedCategory.p` `CategoryTheory.Functor.obj` `CategoryTheory.instCategoryObj` `toFunctor` `CategoryTheory.Functor.map`	—	`isHomLift_map` `preserves_isHomLift`
`isHomLift_map` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.BasedCategory.obj` `CategoryTheory.BasedCategory.category` `CategoryTheory.BasedCategory.p`	—	`CategoryTheory.IsHomLift.of_fac` `CategoryTheory.IsHomLift.domain_eq` `w_obj` `CategoryTheory.IsHomLift.codomain_eq` `CategoryTheory.Functor.congr_obj` `w` `CategoryTheory.IsHomLift.fac` `CategoryTheory.Functor.congr_hom` `CategoryTheory.Category.assoc` `CategoryTheory.eqToHom_trans` `CategoryTheory.eqToHom_trans_assoc`
`preserves_isHomLift` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.BasedCategory.obj` `CategoryTheory.BasedCategory.category` `CategoryTheory.BasedCategory.p` `CategoryTheory.Functor.obj` `CategoryTheory.instCategoryObj` `toFunctor` `CategoryTheory.Functor.map`	—	`CategoryTheory.IsHomLift.of_fac` `w_obj` `CategoryTheory.IsHomLift.domain_eq` `CategoryTheory.IsHomLift.codomain_eq` `CategoryTheory.Functor.comp_map` `CategoryTheory.Functor.congr_obj` `w` `CategoryTheory.Functor.congr_hom` `CategoryTheory.Category.assoc` `CategoryTheory.eqToHom_trans` `CategoryTheory.eqToHom_trans_assoc` `CategoryTheory.IsHomLift.fac`
`w` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj` `toFunctor` `CategoryTheory.BasedCategory.p`	—	—
`w_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.BasedCategory.obj` `CategoryTheory.BasedCategory.category` `CategoryTheory.BasedCategory.p` `CategoryTheory.instCategoryObj` `toFunctor`	—	`CategoryTheory.Functor.comp_obj` `w`

CategoryTheory.BasedNatIso

Definitions

Name	Category	Theorems
`id` 📖	CompOp	2 math math: `id_hom`, `id_inv`
`mkNatIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`id_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.BasedFunctor` `CategoryTheory.BasedNatTrans.homCategory` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`id_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.BasedFunctor` `CategoryTheory.BasedNatTrans.homCategory` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`isIso_of_toNatTrans_isIso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.BasedFunctor` `CategoryTheory.BasedNatTrans.homCategory`	—	`CategoryTheory.Functor.ReflectsIsomorphisms.reflects` `CategoryTheory.BasedNatTrans.instReflectsIsomorphismsBasedFunctorFunctorObjForgetful`

CategoryTheory.BasedNatTrans

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	2 math math: `comp_toNatTrans`, `homCategory_comp`
`forgetful` 📖	CompOp	3 math math: `forgetful_map`, `instReflectsIsomorphismsBasedFunctorFunctorObjForgetful`, `forgetful_obj`
`homCategory` 📖	CompOp	8 math math: `CategoryTheory.BasedNatIso.id_hom`, `CategoryTheory.BasedNatIso.isIso_of_toNatTrans_isIso`, `forgetful_map`, `CategoryTheory.BasedNatIso.id_inv`, `homCategory_comp`, `instReflectsIsomorphismsBasedFunctorFunctorObjForgetful`, `homCategory_id`, `forgetful_obj`
`id` 📖	CompOp	2 math math: `id_toNatTrans`, `homCategory_id`
`toNatTrans` 📖	CompOp	11 math math: `id_toNatTrans`, `isHomLift'`, `CategoryTheory.BasedCategory.whiskerLeft_toNatTrans`, `CategoryTheory.BasedCategory.whiskerRight_toNatTrans`, `homCategory.ext_iff`, `forgetful_map`, `comp_toNatTrans`, `instIsIsoFunctorObjOfBasedFunctor`, `ext_iff`, `app_isHomLift`, `isHomLift`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`app_isHomLift` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.BasedCategory.obj` `CategoryTheory.BasedCategory.category` `CategoryTheory.BasedCategory.p` `CategoryTheory.Functor.obj` `CategoryTheory.instCategoryObj` `CategoryTheory.BasedFunctor.toFunctor` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `toNatTrans`	—	`isHomLift'`
`comp_toNatTrans` 📖	mathematical	—	`toNatTrans` `comp` `CategoryTheory.NatTrans.vcomp` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj` `CategoryTheory.BasedFunctor.toFunctor`	—	—
`ext` 📖	—	`toNatTrans`	—	—	—
`ext_iff` 📖	mathematical	—	`toNatTrans`	—	`ext`
`forgetful_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.BasedFunctor` `homCategory` `CategoryTheory.Functor` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj` `CategoryTheory.Functor.category` `forgetful` `toNatTrans`	—	—
`forgetful_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.BasedFunctor` `homCategory` `CategoryTheory.Functor` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj` `CategoryTheory.Functor.category` `forgetful` `CategoryTheory.BasedFunctor.toFunctor`	—	—
`homCategory_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.BasedFunctor` `CategoryTheory.Category.toCategoryStruct` `homCategory` `comp`	—	—
`homCategory_id` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `CategoryTheory.BasedFunctor` `CategoryTheory.Category.toCategoryStruct` `homCategory` `id`	—	—
`id_toNatTrans` 📖	mathematical	—	`toNatTrans` `id` `CategoryTheory.NatTrans.id` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj` `CategoryTheory.BasedFunctor.toFunctor`	—	—
`instIsIsoFunctorObjOfBasedFunctor` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj` `CategoryTheory.Functor.category` `CategoryTheory.BasedFunctor.toFunctor` `toNatTrans`	—	`forgetful_map` `CategoryTheory.Functor.map_isIso`
`instReflectsIsomorphismsBasedFunctorFunctorObjForgetful` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `CategoryTheory.BasedFunctor` `homCategory` `CategoryTheory.Functor` `CategoryTheory.BasedCategory.obj` `CategoryTheory.instCategoryObj` `CategoryTheory.Functor.category` `forgetful`	—	`CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.NatIso.isIso_inv_app` `app_isHomLift` `homCategory.ext` `CategoryTheory.NatTrans.ext` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.IsIso.inv_hom_id`
`isHomLift` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.BasedCategory.obj` `CategoryTheory.BasedCategory.category` `CategoryTheory.BasedCategory.p`	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.instCategoryObj` `CategoryTheory.BasedFunctor.toFunctor` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `toNatTrans`	—	`app_isHomLift`
`isHomLift'` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.BasedCategory.obj` `CategoryTheory.BasedCategory.category` `CategoryTheory.BasedCategory.p` `CategoryTheory.Functor.obj` `CategoryTheory.instCategoryObj` `CategoryTheory.BasedFunctor.toFunctor` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `toNatTrans`	—	—

CategoryTheory.BasedNatTrans.homCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.BasedNatTrans.toNatTrans`	—	—	`CategoryTheory.BasedNatTrans.ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.BasedNatTrans.toNatTrans`	—	`ext`

---

← Back to Index