Functor

📁 Source: Mathlib/CategoryTheory/Monoidal/Rigid/Functor.lean

Statistics

Metric	Count
Definitions leftDualFunctor, rightDualFunctor	2
Theorems leftDualFunctor_map, leftDualFunctor_obj, rightDualFunctor_map, rightDualFunctor_obj	4
Total	6

CategoryTheory

Definitions

Name	Category	Theorems
leftDualFunctor 📖	CompOp	2 math math: leftDualFunctor_obj, leftDualFunctor_map
rightDualFunctor 📖	CompOp	2 math math: rightDualFunctor_map, rightDualFunctor_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftDualFunctor_map 📖	mathematical	—	Functor.map MonoidalOpposite Opposite MonoidalOpposite.monoidalOppositeCategory Category.opposite leftDualFunctor Quiver.Hom.mop Opposite.op HasLeftDual.leftDual LeftRigidCategory.leftDual Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct leftAdjointMate	—	—
leftDualFunctor_obj 📖	mathematical	—	Functor.obj MonoidalOpposite Opposite MonoidalOpposite.monoidalOppositeCategory Category.opposite leftDualFunctor MonoidalOpposite.mop Opposite.op HasLeftDual.leftDual LeftRigidCategory.leftDual	—	—
rightDualFunctor_map 📖	mathematical	—	Functor.map MonoidalOpposite Opposite MonoidalOpposite.monoidalOppositeCategory Category.opposite rightDualFunctor Quiver.Hom.mop Opposite.op HasRightDual.rightDual RightRigidCategory.rightDual Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct rightAdjointMate	—	—
rightDualFunctor_obj 📖	mathematical	—	Functor.obj MonoidalOpposite Opposite MonoidalOpposite.monoidalOppositeCategory Category.opposite rightDualFunctor MonoidalOpposite.mop Opposite.op HasRightDual.rightDual RightRigidCategory.rightDual	—	—

---

← Back to Index