Documentation Verification Report

Multifunctor

📁 Source: Mathlib/CategoryTheory/Monoidal/Multifunctor.lean

Statistics

Metric	Count
Definitions `ofBifunctor`, `ofBifunctor`, `bottomMapᵣ`, `bottomMapₗ`, `firstMap`, `firstMap₁`, `firstMap₂`, `firstMap₃`, `leftMapᵣ`, `leftMapₗ`, `secondMap`, `secondMap₁`, `secondMap₂`, `secondMap₃`, `topMapᵣ`, `topMapₗ`, `ofBifunctor`, `ofBifunctor`, `bottomMapᵣ`, `bottomMapₗ`, `firstMap`, `firstMap₁`, `firstMap₂`, `firstMap₃`, `leftMapᵣ`, `leftMapₗ`, `secondMap`, `secondMap₁`, `secondMap₂`, `secondMap₃`, `topMapᵣ`, `topMapₗ`, `curriedTensorPreIsoPost`, `curriedTensorInsertFunctor₁`, `curriedTensorInsertFunctor₂`, `curriedTensorPost`, `curriedTensorPostFunctor`, `curriedTensorPostPost`, `curriedTensorPostPost'`, `curriedTensorPostPre`, `curriedTensorPre`, `curriedTensorPreFunctor`, `curriedTensorPrePost`, `curriedTensorPrePre`, `curriedTensorPrePre'`	45
Theorems `bottomMapᵣ_app`, `bottomMapₗ_app`, `firstMap_app_app_app`, `firstMap₁_app_app_app`, `firstMap₂_app_app_app`, `firstMap₃_app_app_app`, `leftMapᵣ_app`, `leftMapₗ_app`, `secondMap_app_app_app`, `secondMap₁_app_app_app`, `secondMap₂_app_app_app`, `secondMap₃_app_app_app`, `topMapᵣ_app`, `topMapₗ_app`, `bottomMapᵣ_app`, `bottomMapₗ_app`, `firstMap_app_app_app`, `firstMap₁_app_app_app`, `firstMap₂_app_app_app`, `firstMap₃_app_app_app`, `leftMapᵣ_app`, `leftMapₗ_app`, `secondMap_app_app_app`, `secondMap₁_app_app_app`, `secondMap₂_app_app_app`, `secondMap₃_app_app_app`, `topMapᵣ_app`, `topMapₗ_app`, `curriedTensorPreIsoPost_hom_app_app`, `curriedTensorPreIsoPost_inv_app_app`, `curriedTensorPreFunctor_map_app_app`, `curriedTensorPreFunctor_obj`	32
Total	77

CategoryTheory.Functor.CoreMonoidal

Definitions

Name	Category	Theorems
`ofBifunctor` 📖	CompOp	—

CategoryTheory.Functor.LaxMonoidal

Definitions

Name	Category	Theorems
`ofBifunctor` 📖	CompOp	—

CategoryTheory.Functor.LaxMonoidal.ofBifunctor

Definitions

Name	Category	Theorems
`bottomMapᵣ` 📖	CompOp	1 math math: `bottomMapᵣ_app`
`bottomMapₗ` 📖	CompOp	1 math math: `bottomMapₗ_app`
`firstMap` 📖	CompOp	1 math math: `firstMap_app_app_app`
`firstMap₁` 📖	CompOp	1 math math: `firstMap₁_app_app_app`
`firstMap₂` 📖	CompOp	1 math math: `firstMap₂_app_app_app`
`firstMap₃` 📖	CompOp	1 math math: `firstMap₃_app_app_app`
`leftMapᵣ` 📖	CompOp	1 math math: `leftMapᵣ_app`
`leftMapₗ` 📖	CompOp	1 math math: `leftMapₗ_app`
`secondMap` 📖	CompOp	1 math math: `secondMap_app_app_app`
`secondMap₁` 📖	CompOp	1 math math: `secondMap₁_app_app_app`
`secondMap₂` 📖	CompOp	1 math math: `secondMap₂_app_app_app`
`secondMap₃` 📖	CompOp	1 math math: `secondMap₃_app_app_app`
`topMapᵣ` 📖	CompOp	1 math math: `topMapᵣ_app`
`topMapₗ` 📖	CompOp	1 math math: `topMapₗ_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bottomMapᵣ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `bottomMapᵣ` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`bottomMapₗ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `bottomMapₗ` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—
`firstMap_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensorPrePre` `CategoryTheory.MonoidalCategory.curriedTensorPostPost'` `firstMap` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`firstMap₁_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₁₂FunctorObj` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₂` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPrePre` `CategoryTheory.MonoidalCategory.curriedTensorPostPre` `firstMap₁` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj`	—	—
`firstMap₂_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPostPre` `CategoryTheory.MonoidalCategory.curriedTensorPostPost` `firstMap₂` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`firstMap₃_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.MonoidalCategory.curriedTensorPostPost` `CategoryTheory.MonoidalCategory.curriedTensorPostPost'` `firstMap₃` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`leftMapᵣ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorUnitRight` `leftMapᵣ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`leftMapₗ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorUnitLeft` `leftMapₗ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—
`secondMap_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensorPrePre` `CategoryTheory.MonoidalCategory.curriedTensorPostPost'` `secondMap` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPost`	—	—
`secondMap₁_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.Functor.whiskeringLeft₂` `CategoryTheory.MonoidalCategory.curriedTensorPrePre` `CategoryTheory.MonoidalCategory.curriedTensorPrePre'` `secondMap₁` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`secondMap₂_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₁` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPrePre'` `CategoryTheory.MonoidalCategory.curriedTensorPrePost` `secondMap₂` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj`	—	—
`secondMap₃_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₂₃FunctorObj` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPrePost` `CategoryTheory.MonoidalCategory.curriedTensorPostPost'` `secondMap₃` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`topMapᵣ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorUnitRight` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `topMapᵣ` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	—
`topMapₗ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorUnitLeft` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `topMapₗ` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	—

CategoryTheory.Functor.Monoidal

Definitions

Name	Category	Theorems
`ofBifunctor` 📖	CompOp	—

CategoryTheory.Functor.OplaxMonoidal

Definitions

Name	Category	Theorems
`ofBifunctor` 📖	CompOp	—

CategoryTheory.Functor.OplaxMonoidal.ofBifunctor

Definitions

Name	Category	Theorems
`bottomMapᵣ` 📖	CompOp	1 math math: `bottomMapᵣ_app`
`bottomMapₗ` 📖	CompOp	1 math math: `bottomMapₗ_app`
`firstMap` 📖	CompOp	1 math math: `firstMap_app_app_app`
`firstMap₁` 📖	CompOp	1 math math: `firstMap₁_app_app_app`
`firstMap₂` 📖	CompOp	1 math math: `firstMap₂_app_app_app`
`firstMap₃` 📖	CompOp	1 math math: `firstMap₃_app_app_app`
`leftMapᵣ` 📖	CompOp	1 math math: `leftMapᵣ_app`
`leftMapₗ` 📖	CompOp	1 math math: `leftMapₗ_app`
`secondMap` 📖	CompOp	1 math math: `secondMap_app_app_app`
`secondMap₁` 📖	CompOp	1 math math: `secondMap₁_app_app_app`
`secondMap₂` 📖	CompOp	1 math math: `secondMap₂_app_app_app`
`secondMap₃` 📖	CompOp	1 math math: `secondMap₃_app_app_app`
`topMapᵣ` 📖	CompOp	1 math math: `topMapᵣ_app`
`topMapₗ` 📖	CompOp	1 math math: `topMapₗ_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bottomMapᵣ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorUnitRight` `bottomMapᵣ` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	—
`bottomMapₗ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorUnitLeft` `bottomMapₗ` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	—
`firstMap_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensorPostPost` `CategoryTheory.MonoidalCategory.curriedTensorPrePre'` `firstMap` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`firstMap₁_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPostPost` `CategoryTheory.MonoidalCategory.curriedTensorPostPre` `firstMap₁` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`firstMap₂_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₁₂FunctorObj` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₂` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPostPre` `CategoryTheory.MonoidalCategory.curriedTensorPrePre` `firstMap₂` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj`	—	—
`firstMap₃_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.Functor.whiskeringLeft₂` `CategoryTheory.MonoidalCategory.curriedTensorPrePre` `CategoryTheory.MonoidalCategory.curriedTensorPrePre'` `firstMap₃` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`leftMapᵣ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorUnitRight` `leftMapᵣ` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`leftMapₗ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.MonoidalCategory.tensorUnitLeft` `leftMapₗ` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—
`secondMap_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensorPostPost` `CategoryTheory.MonoidalCategory.curriedTensorPrePre'` `secondMap` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	—
`secondMap₁_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.MonoidalCategory.curriedTensorPostPost` `CategoryTheory.MonoidalCategory.curriedTensorPostPost'` `secondMap₁` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`secondMap₂_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₂₃FunctorObj` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPostPost'` `CategoryTheory.MonoidalCategory.curriedTensorPrePost` `secondMap₂` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`secondMap₃_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₁` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPrePost` `CategoryTheory.MonoidalCategory.curriedTensorPrePre'` `secondMap₃` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj`	—	—
`topMapᵣ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `topMapᵣ` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`topMapₗ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `topMapₗ` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—

CategoryTheory.MonoidalCategory

Definitions

Name	Category	Theorems
`curriedTensorInsertFunctor₁` 📖	CompOp	2 math math: `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂_app_app_app`
`curriedTensorInsertFunctor₂` 📖	CompOp	2 math math: `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁_app_app_app`
`curriedTensorPost` 📖	CompOp	20 math math: `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂_app_app_app`, `CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app`, `CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app'`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap_app_app_app`, `CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_inv`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁_app_app_app`, `CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_hom`, `CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂_app_app_app`, `Functor.curriedTensorPreIsoPost_hom_app_app`, `Functor.curriedTensorPreIsoPost_inv_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap_app_app_app`, `CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap_app_app_app`
`curriedTensorPostFunctor` 📖	CompOp	1 math math: `CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso`
`curriedTensorPostPost` 📖	CompOp	6 math math: `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₁_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap_app_app_app`
`curriedTensorPostPost'` 📖	CompOp	6 math math: `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₁_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap_app_app_app`
`curriedTensorPostPre` 📖	CompOp	4 math math: `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂_app_app_app`
`curriedTensorPre` 📖	CompOp	27 math math: `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂_app_app_app`, `CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ_app`, `CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app'`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap_app_app_app`, `curriedTensorPreFunctor_obj`, `CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_inv`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁_app_app_app`, `CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_hom`, `CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂_app_app_app`, `Functor.curriedTensorPreIsoPost_hom_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ_app`, `Functor.curriedTensorPreIsoPost_inv_app_app`, `CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre_iso`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap_app_app_app`, `CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc`, `curriedTensorPreFunctor_map_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap_app_app_app`
`curriedTensorPreFunctor` 📖	CompOp	3 math math: `curriedTensorPreFunctor_obj`, `CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre_iso`, `curriedTensorPreFunctor_map_app_app`
`curriedTensorPrePost` 📖	CompOp	4 math math: `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃_app_app_app`
`curriedTensorPrePre` 📖	CompOp	6 math math: `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₃_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap_app_app_app`
`curriedTensorPrePre'` 📖	CompOp	6 math math: `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap_app_app_app`, `CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₃_app_app_app`, `CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap_app_app_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curriedTensorPreFunctor_map_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedTensorPre` `CategoryTheory.Functor.map` `curriedTensorPreFunctor` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `toMonoidalCategoryStruct`	—	—
`curriedTensorPreFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedTensorPreFunctor` `curriedTensorPre`	—	—

CategoryTheory.MonoidalCategory.Functor

Definitions

Name	Category	Theorems
`curriedTensorPreIsoPost` 📖	CompOp	3 math math: `CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso`, `curriedTensorPreIsoPost_hom_app_app`, `curriedTensorPreIsoPost_inv_app_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curriedTensorPreIsoPost_hom_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.Iso.hom` `curriedTensorPreIsoPost` `CategoryTheory.Functor.LaxMonoidal.μ` `CategoryTheory.Functor.Monoidal.toLaxMonoidal`	—	—
`curriedTensorPreIsoPost_inv_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensorPost` `CategoryTheory.MonoidalCategory.curriedTensorPre` `CategoryTheory.Iso.inv` `curriedTensorPreIsoPost` `CategoryTheory.Functor.OplaxMonoidal.δ` `CategoryTheory.Functor.Monoidal.toOplaxMonoidal`	—	—

---

← Back to Index