Documentation Verification Report

End

📁 Source: Mathlib/CategoryTheory/Monoidal/Action/End.lean

Statistics

Metric	Count
Definitions `actionOfMonoidalFunctorToEndofunctorMop`, `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso`, `curriedActionMop`, `curriedActionMopMonoidal`, `actionOfMonoidalFunctorToEndofunctor`, `curriedActionActionOfMonoidalFunctorToEndofunctorIso`, `curriedActionMonoidal`, `evaluationRightAction`	8
Theorems `actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom`, `actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv`, `actionOfMonoidalFunctorToEndofunctorMop_actionHom`, `actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft`, `actionOfMonoidalFunctorToEndofunctorMop_actionHomRight`, `actionOfMonoidalFunctorToEndofunctorMop_actionObj`, `actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom`, `actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv`, `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app`, `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app`, `curriedActionMopMonoidal_δ_unmop_app`, `curriedActionMopMonoidal_ε_unmop_app`, `curriedActionMopMonoidal_η_unmop_app`, `curriedActionMopMonoidal_μ_unmop_app`, `curriedActionMop_map_unmop_app`, `curriedActionMop_obj_unmop_map`, `curriedActionMop_obj_unmop_obj`, `actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom`, `actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv`, `actionOfMonoidalFunctorToEndofunctor_actionHom`, `actionOfMonoidalFunctorToEndofunctor_actionHomLeft`, `actionOfMonoidalFunctorToEndofunctor_actionHomRight`, `actionOfMonoidalFunctorToEndofunctor_actionObj`, `actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom`, `actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv`, `curriedActionActionOfMonoidalFunctorToEndofunctorIso_hom_app_app`, `curriedActionActionOfMonoidalFunctorToEndofunctorIso_inv_app_app`, `curriedActionMonoidal_δ_app`, `curriedActionMonoidal_ε_app`, `curriedActionMonoidal_η_app`, `curriedActionMonoidal_μ_app`, `evaluationRightAction_actionAssocIso`, `evaluationRightAction_actionHomLeft`, `evaluationRightAction_actionHomRight`, `evaluationRightAction_actionObj`, `evaluationRightAction_actionUnitIso`	36
Total	44

CategoryTheory.MonoidalCategory.MonoidalLeftAction

Definitions

Name	Category	Theorems
`actionOfMonoidalFunctorToEndofunctorMop` 📖	CompOp	10 math math: `actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft`, `actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom`, `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app`, `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app`, `actionOfMonoidalFunctorToEndofunctorMop_actionObj`, `actionOfMonoidalFunctorToEndofunctorMop_actionHomRight`, `actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom`, `actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv`, `actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv`, `actionOfMonoidalFunctorToEndofunctorMop_actionHom`
`curriedActionActionOfMonoidalFunctorToEndofunctorMopIso` 📖	CompOp	2 math math: `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app`, `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app`
`curriedActionMop` 📖	CompOp	9 math math: `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app`, `curriedActionMopMonoidal_μ_unmop_app`, `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app`, `curriedActionMop_map_unmop_app`, `curriedActionMopMonoidal_δ_unmop_app`, `curriedActionMop_obj_unmop_obj`, `curriedActionMop_obj_unmop_map`, `curriedActionMopMonoidal_η_unmop_app`, `curriedActionMopMonoidal_ε_unmop_app`
`curriedActionMopMonoidal` 📖	CompOp	4 math math: `curriedActionMopMonoidal_μ_unmop_app`, `curriedActionMopMonoidal_δ_unmop_app`, `curriedActionMopMonoidal_η_unmop_app`, `curriedActionMopMonoidal_ε_unmop_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.monoidalCategoryMop` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `toMonoidalLeftActionStruct` `actionOfMonoidalFunctorToEndofunctorMop` `CategoryTheory.NatTrans.app` `Quiver.Hom.unmop` `CategoryTheory.Functor.OplaxMonoidal.δ` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal`	—	—
`actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.monoidalCategoryMop` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `toMonoidalLeftActionStruct` `actionOfMonoidalFunctorToEndofunctorMop` `CategoryTheory.NatTrans.app` `Quiver.Hom.unmop` `CategoryTheory.Functor.LaxMonoidal.μ` `CategoryTheory.Functor.Monoidal.toLaxMonoidal`	—	—
`actionOfMonoidalFunctorToEndofunctorMop_actionHom` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `actionOfMonoidalFunctorToEndofunctorMop` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `CategoryTheory.NatTrans.app` `Quiver.Hom.unmop` `CategoryTheory.Functor.map`	—	—
`actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `actionOfMonoidalFunctorToEndofunctorMop` `CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `Quiver.Hom.unmop` `CategoryTheory.Functor.map`	—	—
`actionOfMonoidalFunctorToEndofunctorMop_actionHomRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `actionOfMonoidalFunctorToEndofunctorMop` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category`	—	—
`actionOfMonoidalFunctorToEndofunctorMop_actionObj` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `actionOfMonoidalFunctorToEndofunctorMop` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category`	—	—
`actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.monoidalCategoryMop` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `toMonoidalLeftActionStruct` `actionOfMonoidalFunctorToEndofunctorMop` `CategoryTheory.NatTrans.app` `Quiver.Hom.unmop` `CategoryTheory.Functor.OplaxMonoidal.η` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal`	—	—
`actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.monoidalCategoryMop` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `toMonoidalLeftActionStruct` `actionOfMonoidalFunctorToEndofunctorMop` `CategoryTheory.NatTrans.app` `Quiver.Hom.unmop` `CategoryTheory.Functor.LaxMonoidal.ε` `CategoryTheory.Functor.Monoidal.toLaxMonoidal`	—	—
`curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `curriedActionMop` `actionOfMonoidalFunctorToEndofunctorMop` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom` `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso` `CategoryTheory.CategoryStruct.id`	—	—
`curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `curriedActionMop` `actionOfMonoidalFunctorToEndofunctorMop` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.inv` `curriedActionActionOfMonoidalFunctorToEndofunctorMopIso` `CategoryTheory.CategoryStruct.id`	—	—
`curriedActionMopMonoidal_δ_unmop_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `curriedActionMop` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalOpposite.mop` `CategoryTheory.Functor.OplaxMonoidal.δ` `CategoryTheory.monoidalCategoryMop` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `curriedActionMopMonoidal` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso`	—	—
`curriedActionMopMonoidal_ε_unmop_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `actionLeft` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalOpposite.unmop` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalOpposite.mop` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.Functor.obj` `curriedAction` `CategoryTheory.Functor.LaxMonoidal.ε` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.monoidalCategoryMop` `curriedActionMop` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `curriedActionMopMonoidal` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	—
`curriedActionMopMonoidal_η_unmop_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `actionLeft` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.MonoidalOpposite.unmop` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalOpposite.mop` `CategoryTheory.Functor.obj` `curriedAction` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.Functor.OplaxMonoidal.η` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.monoidalCategoryMop` `curriedActionMop` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `curriedActionMopMonoidal` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	—
`curriedActionMopMonoidal_μ_unmop_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `curriedActionMop` `curriedAction` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalOpposite.mop` `CategoryTheory.Functor.LaxMonoidal.μ` `CategoryTheory.monoidalCategoryMop` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `curriedActionMopMonoidal` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso`	—	—
`curriedActionMop_map_unmop_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `curriedActionMop` `Quiver.Hom.unmop` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—
`curriedActionMop_obj_unmop_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `curriedActionMop` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—
`curriedActionMop_obj_unmop_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.MonoidalOpposite.unmop` `CategoryTheory.Functor` `CategoryTheory.MonoidalOpposite` `CategoryTheory.MonoidalOpposite.monoidalOppositeCategory` `CategoryTheory.Functor.category` `curriedActionMop` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—

CategoryTheory.MonoidalCategory.MonoidalRightAction

Definitions

Name	Category	Theorems
`actionOfMonoidalFunctorToEndofunctor` 📖	CompOp	10 math math: `curriedActionActionOfMonoidalFunctorToEndofunctorIso_inv_app_app`, `actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv`, `actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom`, `actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv`, `curriedActionActionOfMonoidalFunctorToEndofunctorIso_hom_app_app`, `actionOfMonoidalFunctorToEndofunctor_actionObj`, `actionOfMonoidalFunctorToEndofunctor_actionHomRight`, `actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom`, `actionOfMonoidalFunctorToEndofunctor_actionHomLeft`, `actionOfMonoidalFunctorToEndofunctor_actionHom`
`curriedActionActionOfMonoidalFunctorToEndofunctorIso` 📖	CompOp	2 math math: `curriedActionActionOfMonoidalFunctorToEndofunctorIso_inv_app_app`, `curriedActionActionOfMonoidalFunctorToEndofunctorIso_hom_app_app`
`curriedActionMonoidal` 📖	CompOp	4 math math: `curriedActionMonoidal_η_app`, `curriedActionMonoidal_ε_app`, `curriedActionMonoidal_μ_app`, `curriedActionMonoidal_δ_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `toMonoidalRightActionStruct` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.OplaxMonoidal.δ` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal`	—	—
`actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `toMonoidalRightActionStruct` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.LaxMonoidal.μ` `CategoryTheory.Functor.Monoidal.toLaxMonoidal`	—	—
`actionOfMonoidalFunctorToEndofunctor_actionHom` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map`	—	`CategoryTheory.NatTrans.naturality`
`actionOfMonoidalFunctorToEndofunctor_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.Functor.map` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	—
`actionOfMonoidalFunctorToEndofunctor_actionHomRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map`	—	—
`actionOfMonoidalFunctorToEndofunctor_actionObj` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	—
`actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `toMonoidalRightActionStruct` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.OplaxMonoidal.η` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal`	—	—
`actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `toMonoidalRightActionStruct` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.LaxMonoidal.ε` `CategoryTheory.Functor.Monoidal.toLaxMonoidal`	—	—
`curriedActionActionOfMonoidalFunctorToEndofunctorIso_hom_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.Iso.hom` `curriedActionActionOfMonoidalFunctorToEndofunctorIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`curriedActionActionOfMonoidalFunctorToEndofunctorIso_inv_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `actionOfMonoidalFunctorToEndofunctor` `CategoryTheory.Iso.inv` `curriedActionActionOfMonoidalFunctorToEndofunctorIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`curriedActionMonoidal_δ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.Functor.OplaxMonoidal.δ` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `curriedActionMonoidal` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso`	—	—
`curriedActionMonoidal_ε_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `actionRight` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.LaxMonoidal.ε` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.endofunctorMonoidalCategory` `curriedAction` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `curriedActionMonoidal` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso`	—	—
`curriedActionMonoidal_η_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `actionRight` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Functor.OplaxMonoidal.η` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.endofunctorMonoidalCategory` `curriedAction` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal` `curriedActionMonoidal` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso`	—	—
`curriedActionMonoidal_μ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.Functor.obj` `curriedAction` `CategoryTheory.Functor.LaxMonoidal.μ` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `curriedActionMonoidal` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso`	—	—

CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory

Definitions

Name	Category	Theorems
`evaluationRightAction` 📖	CompOp	5 math math: `evaluationRightAction_actionHomLeft`, `evaluationRightAction_actionUnitIso`, `evaluationRightAction_actionHomRight`, `evaluationRightAction_actionObj`, `evaluationRightAction_actionAssocIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evaluationRightAction_actionAssocIso` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `evaluationRightAction` `CategoryTheory.Iso.symm` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.app` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor.Monoidal.μIso` `CategoryTheory.Functor.id` `CategoryTheory.Functor.Monoidal.instId`	—	—
`evaluationRightAction_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `evaluationRightAction` `CategoryTheory.Functor.map`	—	—
`evaluationRightAction_actionHomRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `evaluationRightAction` `CategoryTheory.NatTrans.app`	—	—
`evaluationRightAction_actionObj` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `evaluationRightAction` `CategoryTheory.Functor.obj`	—	—
`evaluationRightAction_actionUnitIso` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.endofunctorMonoidalCategory` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `evaluationRightAction` `CategoryTheory.Iso.symm` `CategoryTheory.Iso.app` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.Monoidal.εIso` `CategoryTheory.Functor.id` `CategoryTheory.Functor.Monoidal.instId`	—	—

---

← Back to Index