Structures · Category theory
CategoryTheory.MonoidalCategoryStruct
Auxiliary structure to carry only the data fields of (and provide notation for)
MonoidalCategory.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Category
- Shape
- One type argument · adds tensorObj, whiskerLeft, whiskerRight, tensorHom, tensorUnit, associator, leftUnitor, rightUnitor
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances20
- CategoryTheory.Functor
- ModuleCat
- CategoryTheory.Grp
- HomologicalComplex
- CategoryTheory.Mon
- CategoryTheory.ObjectProperty.FullSubcategory
- PresheafOfModules
- AlgCat
- CategoryTheory.AddGrp
- CategoryTheory.AddMon
- QuadraticModuleCat
- SemimoduleCat
- CategoryTheory.Monoidal.Transported
- HopfAlgCat
- BialgCat
- CategoryTheory.WideSubcategory
- CoalgCat
- CategoryTheory.Dial
- CategoryTheory.LocalizedMonoidal
- AugmentedSimplexCategory
How is a type an instance?
Loading the hierarchy index…
Assumed by32
- CategoryTheory.MonoidalCategoryStruct.tensorObj
- CategoryTheory.MonoidalCategoryStruct.tensorUnit
- CategoryTheory.MonoidalCategoryStruct.whiskerLeft
- CategoryTheory.MonoidalCategoryStruct.whiskerRight
- CategoryTheory.MonoidalCategoryStruct.associator
- CategoryTheory.MonoidalCategoryStruct.tensorHom
- CategoryTheory.MonoidalCategoryStruct.leftUnitor
- CategoryTheory.MonoidalCategoryStruct.rightUnitor
- CategoryTheory.Monoidal.InducingFunctorData.μIso
- CategoryTheory.Monoidal.InducingFunctorData.εIso
- CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution
- CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionUnit
- CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution₂
- CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution₂'
- CategoryTheory.MonoidalCategory.Pentagon
- CategoryTheory.Functor.chosenProd
- CategoryTheory.Monoidal.InducingFunctorData.tensorHom_eq
- CategoryTheory.Monoidal.induced
- CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_leftUnitor_hom_eq_leftUnitor_hom
- CategoryTheory.Monoidal.fromInducedCoreMonoidal
- CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_rightUnitor_hom_eq_rightUnitor_hom
- CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_tensorHom_hom_eq_tensorHom
- CategoryTheory.Monoidal.InducingFunctorData.rightUnitor_eq
- CategoryTheory.MonoidalCategory.ofTensorHom
- CategoryTheory.Monoidal.InducingFunctorData.leftUnitor_eq
- CategoryTheory.Monoidal.InducingFunctorData.associator_eq
- CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq
- CategoryTheory.Functor.chosenTerminal
- CategoryTheory.Monoidal.fromInducedMonoidal
- CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq
- CategoryTheory.MonoidalCategory.monoidalOfLawfulDayConvolutionMonoidalCategoryStruct
- CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_associator_hom_eq_associator_hom
Ancestors0
No ancestors.