Documentation Verification Report

SingleObj

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

Statistics

Metric	Count
Definitions `MonoidalSingleObj`, `endMonoidalStarFunctor`, `endMonoidalStarFunctorEquivalence`, `instMonoidalEndMonoidalStarEndMonoidalStarFunctor`, `instBicategoryMonoidalSingleObj`, `instInhabitedMonoidalSingleObj`	6
Theorems `endMonoidalStarFunctorEquivalence_counitIso`, `endMonoidalStarFunctorEquivalence_functor`, `endMonoidalStarFunctorEquivalence_inverse_map`, `endMonoidalStarFunctorEquivalence_inverse_obj`, `endMonoidalStarFunctorEquivalence_unitIso`, `endMonoidalStarFunctor_isEquivalence`, `endMonoidalStarFunctor_map`, `endMonoidalStarFunctor_obj`	8
Total	14

CategoryTheory

Definitions

Name	Category	Theorems
`MonoidalSingleObj` 📖	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`
`instBicategoryMonoidalSingleObj` 📖	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`
`instInhabitedMonoidalSingleObj` 📖	CompOp	—

CategoryTheory.MonoidalSingleObj

Definitions

Name	Category	Theorems
`endMonoidalStarFunctor` 📖	CompOp	5 math math: `endMonoidalStarFunctorEquivalence_counitIso`, `endMonoidalStarFunctor_map`, `endMonoidalStarFunctor_isEquivalence`, `endMonoidalStarFunctor_obj`, `endMonoidalStarFunctorEquivalence_functor`
`endMonoidalStarFunctorEquivalence` 📖	CompOp	5 math math: `endMonoidalStarFunctorEquivalence_counitIso`, `endMonoidalStarFunctorEquivalence_unitIso`, `endMonoidalStarFunctorEquivalence_inverse_map`, `endMonoidalStarFunctorEquivalence_functor`, `endMonoidalStarFunctorEquivalence_inverse_obj`
`instMonoidalEndMonoidalStarEndMonoidalStarFunctor` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`endMonoidalStarFunctorEquivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `CategoryTheory.EndMonoidal` `CategoryTheory.MonoidalSingleObj` `CategoryTheory.instBicategoryMonoidalSingleObj` `star` `endMonoidalStarFunctorEquivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `endMonoidalStarFunctor`	—	—
`endMonoidalStarFunctorEquivalence_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.EndMonoidal` `CategoryTheory.MonoidalSingleObj` `CategoryTheory.instBicategoryMonoidalSingleObj` `star` `endMonoidalStarFunctorEquivalence` `endMonoidalStarFunctor`	—	—
`endMonoidalStarFunctorEquivalence_inverse_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.EndMonoidal` `CategoryTheory.MonoidalSingleObj` `CategoryTheory.instBicategoryMonoidalSingleObj` `star` `CategoryTheory.Equivalence.inverse` `endMonoidalStarFunctorEquivalence`	—	—
`endMonoidalStarFunctorEquivalence_inverse_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.EndMonoidal` `CategoryTheory.MonoidalSingleObj` `CategoryTheory.instBicategoryMonoidalSingleObj` `star` `CategoryTheory.Equivalence.inverse` `endMonoidalStarFunctorEquivalence`	—	—
`endMonoidalStarFunctorEquivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `CategoryTheory.EndMonoidal` `CategoryTheory.MonoidalSingleObj` `CategoryTheory.instBicategoryMonoidalSingleObj` `star` `endMonoidalStarFunctorEquivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id`	—	—
`endMonoidalStarFunctor_isEquivalence` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.EndMonoidal` `CategoryTheory.MonoidalSingleObj` `CategoryTheory.instBicategoryMonoidalSingleObj` `star` `endMonoidalStarFunctor`	—	`CategoryTheory.Equivalence.isEquivalence_functor`
`endMonoidalStarFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.EndMonoidal` `CategoryTheory.MonoidalSingleObj` `CategoryTheory.instBicategoryMonoidalSingleObj` `star` `endMonoidalStarFunctor`	—	—
`endMonoidalStarFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.EndMonoidal` `CategoryTheory.MonoidalSingleObj` `CategoryTheory.instBicategoryMonoidalSingleObj` `star` `endMonoidalStarFunctor`	—	—

---

← Back to Index