Monoidal

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

Statistics

Metric	Count
Definitions Monoidal, HasGoodTensorTensor₂₃, HasGoodTensor₁₂Tensor, HasLeftTensor₃ObjExt, HasTensor, HasTensor₄ObjExt, associator, isInitialTensorUnitApply, leftUnitor, rightUnitor, r₁₂₃, tensorHom, tensorIso, tensorObj, tensorObjDesc, tensorUnit, tensorUnit₀, triangleIndexData, whiskerLeft, whiskerRight, ιTensorObj, ιTensorObj₃, ιTensorObj₃', ιTensorObj₄, ρ₁₂, ρ₂₃, monoidalCategory	27
Theorems associator_naturality, id_tensorHom_id, instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit, instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1, instHasTensorTensorUnit, instHasTensorTensorUnit_1, leftUnitor_inv_apply, leftUnitor_naturality, leftUnitor_naturality_assoc, left_tensor_tensorObj₃_ext, pentagon, pentagon_inv, pentagon_inv_assoc, rightUnitor_inv_apply, rightUnitor_naturality, rightUnitor_naturality_assoc, tensorHom_comp_tensorHom, tensorHom_comp_tensorHom_assoc, tensorHom_def, tensorIso_hom, tensorIso_inv, tensorObj_ext, tensorObj_ext_iff, tensorObj₃'_ext, tensorObj₃_ext, tensorObj₄_ext, triangle, ιTensorObj₃'_associator_hom, ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃'_eq, ιTensorObj₃'_eq_assoc, ιTensorObj₃'_tensorHom, ιTensorObj₃'_tensorHom_assoc, ιTensorObj₃_associator_inv, ιTensorObj₃_associator_inv_assoc, ιTensorObj₃_eq, ιTensorObj₃_eq_assoc, ιTensorObj₃_tensorHom, ιTensorObj₃_tensorHom_assoc, ιTensorObj₄_eq, ι_tensorHom, ι_tensorHom_assoc, ι_tensorObjDesc, ι_tensorObjDesc_assoc, hasTensor_of_iso, instFiniteElemProdNatPreimageHAddFstSndSingletonSet, instFiniteElemProdNatSetOfEqHAddFstSnd	47
Total	74

CategoryTheory.Functor

Definitions

Name	Category	Theorems
Monoidal 📖	CompData	5 math math: Monoidal.nonempty_monoidal_iff_preservesFiniteProducts, Monoidal.toLaxMonoidal_injective, Braided.toMonoidal_injective, Monoidal.toOplaxMonoidal_injective, Monoidal.instSubsingleton

CategoryTheory.GradedObject

Definitions

Name	Category	Theorems
HasGoodTensorTensor₂₃ 📖	MathDef	—
HasGoodTensor₁₂Tensor 📖	MathDef	—
HasLeftTensor₃ObjExt 📖	MathDef	—
HasTensor 📖	MathDef	4 math math: HomologicalComplex.instHasTensorXTensorUnit_1, Monoidal.instHasTensorTensorUnit_1, Monoidal.instHasTensorTensorUnit, HomologicalComplex.instHasTensorXTensorUnit
HasTensor₄ObjExt 📖	MathDef	—
monoidalCategory 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasTensor_of_iso 📖	—	HasTensor	—	—	hasMap_of_iso
instFiniteElemProdNatPreimageHAddFstSndSingletonSet 📖	mathematical	—	Finite Set.Elem Set.preimage Set Set.instSingletonSet	—	Finite.of_injective Finite.of_fintype
instFiniteElemProdNatSetOfEqHAddFstSnd 📖	mathematical	—	Finite Set.Elem setOf	—	Finite.of_injective Finite.of_fintype

CategoryTheory.GradedObject.Monoidal

Definitions

Name	Category	Theorems
associator 📖	CompOp	11 math math: associator_naturality, pentagon, ιTensorObj₃_associator_inv, pentagon_inv, ιTensorObj₃_associator_inv_assoc, hexagon_reverse, ιTensorObj₃'_associator_hom, hexagon_forward, pentagon_inv_assoc, triangle, ιTensorObj₃'_associator_hom_assoc
isInitialTensorUnitApply 📖	CompOp	—
leftUnitor 📖	CompOp	4 math math: leftUnitor_inv_apply, leftUnitor_naturality, triangle, leftUnitor_naturality_assoc
rightUnitor 📖	CompOp	4 math math: rightUnitor_naturality_assoc, rightUnitor_inv_apply, rightUnitor_naturality, triangle
r₁₂₃ 📖	CompOp	—
tensorHom 📖	CompOp	21 math math: associator_naturality, ιTensorObj₃_tensorHom, ιTensorObj₃_tensorHom_assoc, pentagon, rightUnitor_naturality_assoc, tensorHom_comp_tensorHom, tensorHom_comp_tensorHom_assoc, pentagon_inv, tensorHom_def, id_tensorHom_id, ιTensorObj₃'_tensorHom_assoc, pentagon_inv_assoc, tensorIso_inv, ιTensorObj₃'_tensorHom, rightUnitor_naturality, leftUnitor_naturality, ι_tensorHom_assoc, triangle, leftUnitor_naturality_assoc, tensorIso_hom, ι_tensorHom
tensorIso 📖	CompOp	2 math math: tensorIso_inv, tensorIso_hom
tensorObj 📖	CompOp	21 math math: rightUnitor_naturality_assoc, symmetry, rightUnitor_inv_apply, leftUnitor_inv_apply, tensorHom_comp_tensorHom, symmetry_assoc, tensorHom_comp_tensorHom_assoc, ι_tensorObjDesc_assoc, tensorHom_def, id_tensorHom_id, braiding_naturality_left, ι_tensorObjDesc, braiding_naturality_right, tensorIso_inv, rightUnitor_naturality, leftUnitor_naturality, ι_tensorHom_assoc, leftUnitor_naturality_assoc, tensorIso_hom, ι_tensorHom, tensorObj_ext_iff
tensorObjDesc 📖	CompOp	2 math math: ι_tensorObjDesc_assoc, ι_tensorObjDesc
tensorUnit 📖	CompOp	8 math math: rightUnitor_naturality_assoc, rightUnitor_inv_apply, leftUnitor_inv_apply, instHasTensorTensorUnit_1, instHasTensorTensorUnit, rightUnitor_naturality, leftUnitor_naturality, leftUnitor_naturality_assoc
tensorUnit₀ 📖	CompOp	2 math math: rightUnitor_inv_apply, leftUnitor_inv_apply
triangleIndexData 📖	CompOp	—
whiskerLeft 📖	CompOp	5 math math: tensorHom_def, hexagon_reverse, braiding_naturality_left, braiding_naturality_right, hexagon_forward
whiskerRight 📖	CompOp	5 math math: tensorHom_def, hexagon_reverse, braiding_naturality_left, braiding_naturality_right, hexagon_forward
ιTensorObj 📖	CompOp	12 math math: rightUnitor_inv_apply, leftUnitor_inv_apply, ι_tensorObjDesc_assoc, ι_tensorObjDesc, ιTensorObj₃_eq, ιTensorObj₃_eq_assoc, ιTensorObj₄_eq, ιTensorObj₃'_eq, ι_tensorHom_assoc, ιTensorObj₃'_eq_assoc, ι_tensorHom, tensorObj_ext_iff
ιTensorObj₃ 📖	CompOp	9 math math: ιTensorObj₃_tensorHom, ιTensorObj₃_tensorHom_assoc, ιTensorObj₃_associator_inv, ιTensorObj₃_associator_inv_assoc, ιTensorObj₃'_associator_hom, ιTensorObj₃_eq, ιTensorObj₃_eq_assoc, ιTensorObj₄_eq, ιTensorObj₃'_associator_hom_assoc
ιTensorObj₃' 📖	CompOp	8 math math: ιTensorObj₃_associator_inv, ιTensorObj₃_associator_inv_assoc, ιTensorObj₃'_tensorHom_assoc, ιTensorObj₃'_associator_hom, ιTensorObj₃'_tensorHom, ιTensorObj₃'_eq, ιTensorObj₃'_eq_assoc, ιTensorObj₃'_associator_hom_assoc
ιTensorObj₄ 📖	CompOp	1 math math: ιTensorObj₄_eq
ρ₁₂ 📖	CompOp	—
ρ₂₃ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_naturality 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorHom CategoryTheory.Iso.hom associator	—	CategoryTheory.GradedObject.hom_ext tensorObj₃'_ext ιTensorObj₃'_tensorHom_assoc CategoryTheory.MonoidalCategory.associator_conjugation ιTensorObj₃'_associator_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc ιTensorObj₃'_associator_hom_assoc ιTensorObj₃_tensorHom
id_tensorHom_id 📖	mathematical	CategoryTheory.GradedObject.HasTensor	tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.GradedObject.mapMap_id
instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.GradedObject.HasMap CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.mapBifunctor CategoryTheory.GradedObject.single₀ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	instHasTensorTensorUnit
instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.GradedObject.HasMap CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.mapBifunctor CategoryTheory.GradedObject.single₀ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	instHasTensorTensorUnit_1
instHasTensorTensorUnit 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.GradedObject.HasTensor tensorUnit	—	CategoryTheory.GradedObject.mapBifunctorLeftUnitor_hasMap zero_add
instHasTensorTensorUnit_1 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.GradedObject.HasTensor tensorUnit	—	CategoryTheory.GradedObject.mapBifunctorRightUnitor_hasMap add_zero
leftUnitor_inv_apply 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.Iso.inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorUnit instHasTensorTensorUnit leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.MonoidalCategoryStruct.whiskerRight tensorUnit₀ ιTensorObj zero_add	—	instHasTensorTensorUnit
leftUnitor_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorUnit instHasTensorTensorUnit tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom leftUnitor	—	CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality instHasTensorTensorUnit
leftUnitor_naturality_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorUnit instHasTensorTensorUnit tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom leftUnitor	—	instHasTensorTensorUnit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_naturality
left_tensor_tensorObj₃_ext 📖	—	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft ιTensorObj₃	—	—	CategoryTheory.Limits.IsColimit.hom_ext
pentagon 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ CategoryTheory.GradedObject.HasTensor₄ObjExt	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorHom CategoryTheory.Iso.hom associator CategoryTheory.CategoryStruct.id	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id pentagon_inv_assoc tensorHom_comp_tensorHom_assoc CategoryTheory.Category.comp_id id_tensorHom_id CategoryTheory.Category.id_comp tensorHom_comp_tensorHom
pentagon_inv 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ CategoryTheory.GradedObject.HasTensor₄ObjExt	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv associator	—	CategoryTheory.GradedObject.hom_ext tensorObj₄_ext add_assoc ιTensorObj₄_eq CategoryTheory.Category.assoc ι_tensorHom_assoc CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc ιTensorObj₃_associator_inv ιTensorObj₃'_eq ιTensorObj₃_eq_assoc ιTensorObj₃_associator_inv_assoc ιTensorObj₃'_eq_assoc ι_tensorHom CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.whisker_assoc_symm_assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc ιTensorObj₃_eq CategoryTheory.MonoidalCategory.pentagon_inv_assoc CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.whiskerRight_tensor_assoc
pentagon_inv_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ CategoryTheory.GradedObject.HasTensor₄ObjExt	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pentagon_inv
rightUnitor_inv_apply 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.Iso.inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorUnit instHasTensorTensorUnit_1 rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.MonoidalCategoryStruct.whiskerLeft tensorUnit₀ ιTensorObj add_zero	—	instHasTensorTensorUnit_1
rightUnitor_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorUnit instHasTensorTensorUnit_1 tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom rightUnitor	—	CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality instHasTensorTensorUnit_1
rightUnitor_naturality_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorUnit instHasTensorTensorUnit_1 tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom rightUnitor	—	instHasTensorTensorUnit_1 CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_naturality
tensorHom_comp_tensorHom 📖	mathematical	CategoryTheory.GradedObject.HasTensor	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorHom	—	CategoryTheory.GradedObject.hom_ext tensorObj_ext ι_tensorHom_assoc ι_tensorHom CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc
tensorHom_comp_tensorHom_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_comp_tensorHom
tensorHom_def 📖	mathematical	CategoryTheory.GradedObject.HasTensor	tensorHom CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj whiskerRight whiskerLeft	—	tensorHom_comp_tensorHom CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
tensorIso_hom 📖	mathematical	CategoryTheory.GradedObject.HasTensor	CategoryTheory.Iso.hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorIso tensorHom	—	—
tensorIso_inv 📖	mathematical	CategoryTheory.GradedObject.HasTensor	CategoryTheory.Iso.inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects tensorObj tensorIso tensorHom	—	—
tensorObj_ext 📖	—	CategoryTheory.GradedObject.HasTensor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj ιTensorObj	—	—	CategoryTheory.GradedObject.mapObj_ext
tensorObj_ext_iff 📖	mathematical	CategoryTheory.GradedObject.HasTensor	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj ιTensorObj	—	tensorObj_ext
tensorObj₃'_ext 📖	—	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃'	—	—	CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext
tensorObj₃_ext 📖	—	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃	—	—	CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext
tensorObj₄_ext 📖	—	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ CategoryTheory.GradedObject.HasTensor₄ObjExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₄	—	—	tensorObj_ext left_tensor_tensorObj₃_ext add_assoc ιTensorObj₄_eq CategoryTheory.Category.assoc
triangle 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.GradedObject.HasTensor tensorObj tensorUnit instHasTensorTensorUnit_1 instHasTensorTensorUnit CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.Iso.hom associator tensorHom CategoryTheory.CategoryStruct.id leftUnitor rightUnitor	—	instHasTensorTensorUnit_1 instHasTensorTensorUnit instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1 instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit CategoryTheory.GradedObject.TriangleIndexData.h₃ CategoryTheory.GradedObject.TriangleIndexData.h₁ CategoryTheory.GradedObject.mapBifunctor_triangle CategoryTheory.MonoidalCategory.triangle
ιTensorObj₃'_associator_hom 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃' CategoryTheory.Iso.hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects associator CategoryTheory.MonoidalCategoryStruct.associator ιTensorObj₃	—	CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom
ιTensorObj₃'_associator_hom_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃' CategoryTheory.Iso.hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects associator CategoryTheory.MonoidalCategoryStruct.associator ιTensorObj₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTensorObj₃'_associator_hom
ιTensorObj₃'_eq 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	ιTensorObj₃' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight ιTensorObj	—	—
ιTensorObj₃'_eq_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃' CategoryTheory.MonoidalCategoryStruct.whiskerRight ιTensorObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTensorObj₃'_eq
ιTensorObj₃'_tensorHom 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃' tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom	—	ιTensorObj₃'_eq CategoryTheory.Category.assoc ι_tensorHom CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
ιTensorObj₃'_tensorHom_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃' tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTensorObj₃'_tensorHom
ιTensorObj₃_associator_inv 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃ CategoryTheory.Iso.inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects associator CategoryTheory.MonoidalCategoryStruct.associator ιTensorObj₃'	—	CategoryTheory.GradedObject.ι_mapBifunctorAssociator_inv
ιTensorObj₃_associator_inv_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃ CategoryTheory.Iso.inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects associator CategoryTheory.MonoidalCategoryStruct.associator ιTensorObj₃'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTensorObj₃_associator_inv
ιTensorObj₃_eq 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	ιTensorObj₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft ιTensorObj	—	—
ιTensorObj₃_eq_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃ CategoryTheory.MonoidalCategoryStruct.whiskerLeft ιTensorObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTensorObj₃_eq
ιTensorObj₃_tensorHom 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃ tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom	—	ιTensorObj₃_eq CategoryTheory.Category.assoc ι_tensorHom CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
ιTensorObj₃_tensorHom_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ιTensorObj₃ tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTensorObj₃_tensorHom
ιTensorObj₄_eq 📖	mathematical	CategoryTheory.GradedObject.HasTensor tensorObj AddSemigroup.toAdd AddMonoid.toAddSemigroup	ιTensorObj₄ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft ιTensorObj₃ ιTensorObj	—	—
ι_tensorHom 📖	mathematical	CategoryTheory.GradedObject.HasTensor AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj ιTensorObj tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Category.assoc CategoryTheory.GradedObject.ι_mapBifunctorMapMap
ι_tensorHom_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj ιTensorObj tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_tensorHom
ι_tensorObjDesc 📖	mathematical	CategoryTheory.GradedObject.HasTensor AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj ιTensorObj tensorObjDesc	—	CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc
ι_tensorObjDesc_assoc 📖	mathematical	CategoryTheory.GradedObject.HasTensor AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj ιTensorObj tensorObjDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_tensorObjDesc

---

← Back to Index