Theorems · Definition · category theory
CategoryTheory.MonoidalCategory.curriedTensor
(C : Type u) →
[inst : CategoryTheory.Category.{v, u} C] →
[CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor C (CategoryTheory.Functor C C)The tensor product bifunctor C ⥤ C ⥤ C of a monoidal category.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Category
- Cited by
- 170 results in Mathlib
- Foundations
- Depth 21 from the axioms, rests on 111 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.MonoidalCategoryStruct.tensorObjproof · cited by 3,106
- CategoryTheory.MonoidalCategorystatement and proof · cited by 3,095
- CategoryTheory.MonoidalCategoryStruct.whiskerLeftproof · cited by 915
- CategoryTheory.MonoidalCategoryStruct.whiskerRightproof · cited by 903
Cited by267
Results whose statement or proof uses this declaration.
- CategoryTheory.MonoidalCategory.tensorLeftproof · cited by 170
- CategoryTheory.MonoidalCategory.tensorRightproof · cited by 119
- CategoryTheory.MonoidalCategory.Arrow.pushoutProductproof · cited by 64
- CategoryTheory.GradedObject.Monoidal.tensorObjproof · cited by 54
- CategoryTheory.GradedObject.HasTensorproof · cited by 49
- CategoryTheory.MonoidalCategory.curriedTensorPreproof · cited by 28
- CategoryTheory.GradedObject.Monoidal.ιTensorObjproof · cited by 26
- CategoryTheory.GradedObject.Monoidal.tensorHomproof · cited by 23
- CategoryTheory.MonoidalCategory.curriedTensorPostproof · cited by 21
- CategoryTheory.Localization.Monoidal.tensorBifunctorproof · cited by 19
- CategoryTheory.GradedObject.HasGoodTensorTensor₂₃proof · cited by 15
- CategoryTheory.GradedObject.HasGoodTensor₁₂Tensorproof · cited by 13
Showing the 200 most cited of 267.