Documentation Verification Report

ULift

📁 Source: Mathlib/CategoryTheory/Category/ULift.lean

Statistics

Metric	Count
Definitions `down`, `equiv`, `up`, `downFunctor`, `equivalence`, `upFunctor`, `ULiftHom`, `category`, `down`, `equiv`, `objDown`, `objEquiv`, `objUp`, `up`, `equiv`, `equivCongrLeft`, `objEquiv`, `instInhabitedAsSmall`, `instInhabitedULiftHom`, `instSmallCategoryAsSmall`	20
Theorems `down_map`, `down_obj`, `equiv_counitIso`, `equiv_functor`, `equiv_inverse`, `equiv_unitIso`, `up_map_down`, `up_obj_down`, `downFunctor_map`, `downFunctor_obj`, `equivalence_counitIso_hom_app`, `equivalence_counitIso_inv_app`, `equivalence_functor`, `equivalence_inverse`, `equivalence_unitIso_hom`, `equivalence_unitIso_inv`, `upFunctor_map`, `upFunctor_obj_down`, `down_map`, `down_obj`, `up_map_down`, `up_obj`, `down_comp`, `down_comp_assoc`, `eqToHom_down`, `objDown_objUp`, `objUp_objDown`	27
Total	47

CategoryTheory

Definitions

Name	Category	Theorems
`ULiftHom` 📖	CompOp	11 math math: `ULiftHom.down_map`, `instIsConnectedULiftHomULift`, `ULiftHom.up_map_down`, `instIsCofilteredULiftHom`, `instIsFilteredULiftHom`, `ULiftHom.up_obj`, `CatEnriched.id_eq`, `ULiftHom.down_obj`, `Monoidal.rightUnitor_inv`, `Monoidal.leftUnitor_inv`, `countableCategoryUlift`
`instInhabitedAsSmall` 📖	CompOp	—
`instInhabitedULiftHom` 📖	CompOp	—
`instSmallCategoryAsSmall` 📖	CompOp	26 math math: `Cat.asSmallFunctor_obj`, `down_comp_assoc`, `AsSmall.hasFiniteLimits`, `Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber`, `instIsCofilteredAsSmall`, `AsSmall.down_obj`, `AsSmall.instAdditiveDown`, `AsSmall.equiv_unitIso`, `AsSmall.equiv_counitIso`, `Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber`, `Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber`, `AsSmall.equiv_inverse`, `AsSmall.up_obj_down`, `AsSmall.equiv_functor`, `instIsFilteredAsSmall`, `AsSmall.up_map_down`, `Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base`, `eqToHom_down`, `Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber`, `IsSifted.isSifted_iff_asSmallIsSifted`, `Cat.asSmallFunctor_map`, `AsSmall.instAdditiveUp`, `Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base`, `AsSmall.hasLimitsOfShape`, `AsSmall.down_map`, `down_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_comp` 📖	mathematical	—	`Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `CategoryStruct.comp` `AsSmall` `instSmallCategoryAsSmall`	—	—
`down_comp_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Quiver.Hom` `CategoryStruct.toQuiver` `AsSmall` `instSmallCategoryAsSmall`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `down_comp`
`eqToHom_down` 📖	mathematical	—	`Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `eqToHom` `AsSmall` `instSmallCategoryAsSmall`	—	—
`objDown_objUp` 📖	mathematical	—	`ULiftHom.objDown` `ULiftHom.objUp`	—	—
`objUp_objDown` 📖	mathematical	—	`ULiftHom.objUp` `ULiftHom.objDown`	—	—

CategoryTheory.AsSmall

Definitions

Name	Category	Theorems
`down` 📖	CompOp	11 math math: `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber`, `down_obj`, `instAdditiveDown`, `equiv_unitIso`, `equiv_counitIso`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber`, `equiv_inverse`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber`, `CategoryTheory.Cat.asSmallFunctor_map`, `down_map`
`equiv` 📖	CompOp	4 math math: `equiv_unitIso`, `equiv_counitIso`, `equiv_inverse`, `equiv_functor`
`up` 📖	CompOp	10 math math: `equiv_unitIso`, `equiv_counitIso`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber`, `up_obj_down`, `equiv_functor`, `up_map_down`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber`, `CategoryTheory.Cat.asSmallFunctor_map`, `instAdditiveUp`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.AsSmall` `CategoryTheory.instSmallCategoryAsSmall` `down` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`down_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.AsSmall` `CategoryTheory.instSmallCategoryAsSmall` `down`	—	—
`equiv_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `CategoryTheory.AsSmall` `CategoryTheory.instSmallCategoryAsSmall` `equiv` `CategoryTheory.NatIso.ofComponents` `CategoryTheory.Functor.comp` `down` `up` `CategoryTheory.Functor.id` `CategoryTheory.eqToIso` `CategoryTheory.Functor.obj`	—	—
`equiv_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.AsSmall` `CategoryTheory.instSmallCategoryAsSmall` `equiv` `up`	—	—
`equiv_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CategoryTheory.AsSmall` `CategoryTheory.instSmallCategoryAsSmall` `equiv` `down`	—	—
`equiv_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `CategoryTheory.AsSmall` `CategoryTheory.instSmallCategoryAsSmall` `equiv` `CategoryTheory.NatIso.ofComponents` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `up` `down` `CategoryTheory.eqToIso` `CategoryTheory.Functor.obj`	—	—
`up_map_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.AsSmall` `CategoryTheory.instSmallCategoryAsSmall` `up`	—	—
`up_obj_down` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.AsSmall` `CategoryTheory.instSmallCategoryAsSmall` `up`	—	—

CategoryTheory.ULift

Definitions

Name	Category	Theorems
`downFunctor` 📖	CompOp	7 math math: `equivalence_unitIso_inv`, `equivalence_counitIso_hom_app`, `downFunctor_map`, `equivalence_unitIso_hom`, `equivalence_counitIso_inv_app`, `downFunctor_obj`, `equivalence_inverse`
`equivalence` 📖	CompOp	6 math math: `equivalence_unitIso_inv`, `equivalence_counitIso_hom_app`, `equivalence_unitIso_hom`, `equivalence_functor`, `equivalence_counitIso_inv_app`, `equivalence_inverse`
`upFunctor` 📖	CompOp	7 math math: `upFunctor_obj_down`, `equivalence_unitIso_inv`, `equivalence_counitIso_hom_app`, `equivalence_unitIso_hom`, `equivalence_functor`, `equivalence_counitIso_inv_app`, `upFunctor_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`downFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.uliftCategory` `downFunctor`	—	—
`downFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.uliftCategory` `downFunctor`	—	—
`equivalence_counitIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.uliftCategory` `CategoryTheory.Functor.comp` `downFunctor` `upFunctor` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `equivalence` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`equivalence_counitIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.uliftCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `downFunctor` `upFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `equivalence` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`equivalence_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.uliftCategory` `equivalence` `upFunctor`	—	—
`equivalence_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CategoryTheory.uliftCategory` `equivalence` `downFunctor`	—	—
`equivalence_unitIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.uliftCategory` `upFunctor` `downFunctor` `CategoryTheory.Equivalence.unitIso` `equivalence` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`equivalence_unitIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.uliftCategory` `upFunctor` `downFunctor` `CategoryTheory.Equivalence.unitIso` `equivalence` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`upFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.uliftCategory` `upFunctor`	—	—
`upFunctor_obj_down` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.uliftCategory` `upFunctor`	—	—

CategoryTheory.ULiftHom

Definitions

Name	Category	Theorems
`category` 📖	CompOp	8 math math: `down_map`, `CategoryTheory.instIsConnectedULiftHomULift`, `up_map_down`, `CategoryTheory.instIsCofilteredULiftHom`, `CategoryTheory.instIsFilteredULiftHom`, `up_obj`, `down_obj`, `CategoryTheory.countableCategoryUlift`
`down` 📖	CompOp	2 math math: `down_map`, `down_obj`
`equiv` 📖	CompOp	—
`objDown` 📖	CompOp	5 math math: `CategoryTheory.objUp_objDown`, `down_map`, `up_map_down`, `CategoryTheory.objDown_objUp`, `down_obj`
`objEquiv` 📖	CompOp	—
`objUp` 📖	CompOp	4 math math: `CategoryTheory.objUp_objDown`, `up_map_down`, `CategoryTheory.objDown_objUp`, `up_obj`
`up` 📖	CompOp	2 math math: `up_map_down`, `up_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ULiftHom` `category` `down` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `objDown`	—	—
`down_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ULiftHom` `category` `down` `objDown`	—	—
`up_map_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `objDown` `objUp` `CategoryTheory.Functor.map` `CategoryTheory.ULiftHom` `category` `up`	—	—
`up_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ULiftHom` `category` `up` `objUp`	—	—

CategoryTheory.ULiftHomULiftCategory

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—
`equivCongrLeft` 📖	CompOp	—
`objEquiv` 📖	CompOp	—

---

← Back to Index