Documentation Verification Report

End

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

Statistics

Metric	Count
Definitions `EndMonoidal`, `instCategoryEndMonoidal`, `instInhabitedEndMonoidal`, `instMonoidalCategoryHom`	4
Theorems `associator_def`, `leftUnitor_def`, `rightUnitor_def`, `tensorHom_def`, `tensorObj_def`, `tensorUnit_def`, `whiskerLeft_def`, `whiskerRight_def`	8
Total	12

CategoryTheory

Definitions

Name	Category	Theorems
`EndMonoidal` 📖	CompOp	8 math math: `MonoidalSingleObj.endMonoidalStarFunctorEquivalence_counitIso`, `MonoidalSingleObj.endMonoidalStarFunctor_map`, `MonoidalSingleObj.endMonoidalStarFunctor_isEquivalence`, `MonoidalSingleObj.endMonoidalStarFunctor_obj`, `MonoidalSingleObj.endMonoidalStarFunctorEquivalence_unitIso`, `MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_map`, `MonoidalSingleObj.endMonoidalStarFunctorEquivalence_functor`, `MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_obj`
`instCategoryEndMonoidal` 📖	CompOp	17 math math: `Bicategory.Comonad.comul_assoc_flip`, `whiskerLeft_def`, `whiskerRight_def`, `Bicategory.Comonad.comul_assoc_flip_assoc`, `Bicategory.Comonad.counit_comul_assoc`, `rightUnitor_def`, `tensorHom_def`, `associator_def`, `Bicategory.Comonad.comul_assoc`, `Bicategory.Comonad.counit_def`, `tensorObj_def`, `Bicategory.Comonad.comul_counit_assoc`, `tensorUnit_def`, `Bicategory.Comonad.comul_assoc_assoc`, `Bicategory.Comonad.counit_comul`, `Bicategory.Comonad.comul_counit`, `leftUnitor_def`
`instInhabitedEndMonoidal` 📖	CompOp	—
`instMonoidalCategoryHom` 📖	CompOp	9 math math: `whiskerLeft_def`, `whiskerRight_def`, `rightUnitor_def`, `tensorHom_def`, `associator_def`, `Bicategory.Comonad.counit_def`, `tensorObj_def`, `tensorUnit_def`, `leftUnitor_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_def` 📖	mathematical	—	`MonoidalCategoryStruct.associator` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `instCategoryEndMonoidal` `MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryHom` `Bicategory.associator`	—	—
`leftUnitor_def` 📖	mathematical	—	`MonoidalCategoryStruct.leftUnitor` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `instCategoryEndMonoidal` `MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryHom` `Bicategory.leftUnitor`	—	—
`rightUnitor_def` 📖	mathematical	—	`MonoidalCategoryStruct.rightUnitor` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `instCategoryEndMonoidal` `MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryHom` `Bicategory.rightUnitor`	—	—
`tensorHom_def` 📖	mathematical	—	`MonoidalCategoryStruct.tensorHom` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `instCategoryEndMonoidal` `MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryHom` `CategoryStruct.comp` `Category.toCategoryStruct`	—	—
`tensorObj_def` 📖	mathematical	—	`MonoidalCategoryStruct.tensorObj` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `instCategoryEndMonoidal` `MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryHom` `CategoryStruct.comp`	—	—
`tensorUnit_def` 📖	mathematical	—	`MonoidalCategoryStruct.tensorUnit` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `instCategoryEndMonoidal` `MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryHom` `CategoryStruct.id`	—	—
`whiskerLeft_def` 📖	mathematical	—	`MonoidalCategoryStruct.whiskerLeft` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `instCategoryEndMonoidal` `MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryHom` `Bicategory.whiskerLeft`	—	—
`whiskerRight_def` 📖	mathematical	—	`MonoidalCategoryStruct.whiskerRight` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `instCategoryEndMonoidal` `MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategoryHom` `Bicategory.whiskerRight`	—	—

---

← Back to Index