Monoidal

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

Statistics

Metric	Count
Definitions associatorImpl, braiding, instMonoidalCategory, instMonoidalCategoryStruct, instSymmetricCategory, leftUnitorImpl, rightUnitorImpl, tensorHomImpl, tensorObjImpl, tensorUnitImpl	10
Theorems associatorImpl_hom_F, associatorImpl_hom_f, associatorImpl_inv_F, associatorImpl_inv_f, associator_hom_F, associator_hom_f, associator_inv_F, associator_inv_f, associator_naturality, braiding_hom_F, braiding_hom_f, braiding_inv_F, braiding_inv_f, braiding_naturality_left, braiding_naturality_right, hexagon_forward, hexagon_reverse, id_tensorHom_id, leftUnitorImpl_hom_F, leftUnitorImpl_hom_f, leftUnitorImpl_inv_F, leftUnitorImpl_inv_f, leftUnitor_hom_F, leftUnitor_hom_f, leftUnitor_inv_F, leftUnitor_inv_f, leftUnitor_naturality, pentagon, rightUnitorImpl_hom_F, rightUnitorImpl_hom_f, rightUnitorImpl_inv_F, rightUnitorImpl_inv_f, rightUnitor_hom_F, rightUnitor_hom_f, rightUnitor_inv_F, rightUnitor_inv_f, rightUnitor_naturality, symmetry, tensorHomImpl_F, tensorHomImpl_f, tensorHom_F, tensorHom_comp_tensorHom, tensorHom_f, tensorObjImpl_rel, tensorObjImpl_src, tensorObjImpl_tgt, tensorObj_rel, tensorObj_src, tensorObj_tgt, tensorUnitImpl_rel, tensorUnitImpl_src, tensorUnitImpl_tgt, tensorUnit_rel, tensorUnit_src, tensorUnit_tgt, triangle, whiskerLeft_F, whiskerLeft_f, whiskerRight_F, whiskerRight_f	60
Total	70

CategoryTheory.Dial

Definitions

Name	Category	Theorems
associatorImpl 📖	CompOp	4 math math: associatorImpl_inv_F, associatorImpl_hom_F, associatorImpl_inv_f, associatorImpl_hom_f
braiding 📖	CompOp	9 math math: braiding_inv_f, braiding_naturality_right, hexagon_reverse, braiding_inv_F, braiding_hom_f, hexagon_forward, symmetry, braiding_hom_F, braiding_naturality_left
instMonoidalCategory 📖	CompOp	—
instMonoidalCategoryStruct 📖	CompOp	40 math math: braiding_inv_f, leftUnitor_naturality, tensorUnit_src, rightUnitor_hom_f, rightUnitor_naturality, tensorHom_F, triangle, braiding_naturality_right, associator_hom_F, leftUnitor_hom_f, rightUnitor_hom_F, whiskerRight_f, tensorObj_src, leftUnitor_inv_f, hexagon_reverse, braiding_inv_F, associator_inv_f, braiding_hom_f, rightUnitor_inv_f, leftUnitor_hom_F, whiskerRight_F, hexagon_forward, tensorObj_tgt, associator_naturality, tensorUnit_rel, associator_inv_F, tensorUnit_tgt, pentagon, symmetry, whiskerLeft_f, braiding_hom_F, leftUnitor_inv_F, tensorHom_f, whiskerLeft_F, associator_hom_f, braiding_naturality_left, rightUnitor_inv_F, id_tensorHom_id, tensorHom_comp_tensorHom, tensorObj_rel
instSymmetricCategory 📖	CompOp	—
leftUnitorImpl 📖	CompOp	4 math math: leftUnitorImpl_hom_F, leftUnitorImpl_inv_f, leftUnitorImpl_hom_f, leftUnitorImpl_inv_F
rightUnitorImpl 📖	CompOp	4 math math: rightUnitorImpl_inv_f, rightUnitorImpl_inv_F, rightUnitorImpl_hom_F, rightUnitorImpl_hom_f
tensorHomImpl 📖	CompOp	2 math math: tensorHomImpl_F, tensorHomImpl_f
tensorObjImpl 📖	CompOp	35 math math: tensorObjImpl_rel, rightUnitor_hom_f, rightUnitorImpl_inv_f, tensorHom_F, tensorObjImpl_tgt, associator_hom_F, associatorImpl_inv_F, leftUnitor_hom_f, rightUnitor_hom_F, rightUnitorImpl_inv_F, whiskerRight_f, rightUnitorImpl_hom_F, leftUnitor_inv_f, associator_inv_f, rightUnitor_inv_f, associatorImpl_hom_F, leftUnitor_hom_F, whiskerRight_F, tensorHomImpl_F, associator_inv_F, leftUnitorImpl_hom_F, tensorObjImpl_src, tensorHomImpl_f, whiskerLeft_f, leftUnitor_inv_F, associatorImpl_inv_f, tensorHom_f, whiskerLeft_F, associator_hom_f, leftUnitorImpl_inv_f, associatorImpl_hom_f, rightUnitor_inv_F, leftUnitorImpl_hom_f, rightUnitorImpl_hom_f, leftUnitorImpl_inv_F
tensorUnitImpl 📖	CompOp	19 math math: rightUnitor_hom_f, rightUnitorImpl_inv_f, leftUnitor_hom_f, rightUnitor_hom_F, rightUnitorImpl_inv_F, rightUnitorImpl_hom_F, leftUnitor_inv_f, rightUnitor_inv_f, tensorUnitImpl_src, leftUnitor_hom_F, leftUnitorImpl_hom_F, leftUnitor_inv_F, leftUnitorImpl_inv_f, rightUnitor_inv_F, tensorUnitImpl_rel, leftUnitorImpl_hom_f, rightUnitorImpl_hom_f, leftUnitorImpl_inv_F, tensorUnitImpl_tgt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associatorImpl_hom_F 📖	mathematical	—	Hom.F tensorObjImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory associatorImpl CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.prod.comp_lift
associatorImpl_hom_f 📖	mathematical	—	Hom.f tensorObjImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory associatorImpl CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	—
associatorImpl_inv_F 📖	mathematical	—	Hom.F tensorObjImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory associatorImpl CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.prod.comp_lift
associatorImpl_inv_f 📖	mathematical	—	Hom.f tensorObjImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory associatorImpl CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src CategoryTheory.Limits.prod.fst CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd	—	—
associator_hom_F 📖	mathematical	—	Hom.F tensorObjImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.associator instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.prod.comp_lift
associator_hom_f 📖	mathematical	—	Hom.f tensorObjImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.associator instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	—
associator_inv_F 📖	mathematical	—	Hom.F tensorObjImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.associator instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.prod.comp_lift
associator_inv_f 📖	mathematical	—	Hom.f tensorObjImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.associator instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src CategoryTheory.Limits.prod.fst CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd	—	—
associator_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	hom_ext CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.prod.map_fst_assoc CategoryTheory.Limits.prod.map_fst CategoryTheory.Limits.prod.map_snd CategoryTheory.Limits.prod.lift_fst_comp_snd_comp CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.assoc CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype associator_hom_F CategoryTheory.Limits.prod.map_snd_assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.prod.map_map_assoc CategoryTheory.Limits.prod.lift_map_assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
braiding_hom_F 📖	mathematical	—	Hom.F CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Iso.hom braiding CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.prod.comp_lift
braiding_hom_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Iso.hom braiding CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	—
braiding_inv_F 📖	mathematical	—	Hom.F CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Iso.inv braiding CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.prod.comp_lift
braiding_inv_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Iso.inv braiding CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	—
braiding_naturality_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom braiding	—	CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_tensorHom hom_ext CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.prod.map_snd CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.map_fst CategoryTheory.Limits.prod.lift_map CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype braiding_hom_F CategoryTheory.Limits.prod.map_snd_assoc CategoryTheory.Category.id_comp whiskerRight_F CategoryTheory.Limits.prod.lift_map_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.lift_fst_comp_snd_comp CategoryTheory.Limits.limit.lift_π_assoc whiskerLeft_F CategoryTheory.Limits.prod.map_map_assoc
braiding_naturality_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom braiding	—	CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.tensorHom_id hom_ext CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.prod.map_snd CategoryTheory.Limits.prod.map_fst CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.lift_map CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype braiding_hom_F CategoryTheory.Limits.prod.map_snd_assoc CategoryTheory.Category.id_comp whiskerLeft_F CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.lift_map_assoc CategoryTheory.Limits.prod.lift_fst_comp_snd_comp whiskerRight_F CategoryTheory.Limits.prod.map_map_assoc
hexagon_forward 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator braiding CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_tensorHom hom_ext CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.map_fst_assoc CategoryTheory.Limits.prod.map_snd CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype associator_hom_F CategoryTheory.Limits.prod.map_snd_assoc CategoryTheory.Category.id_comp braiding_hom_F whiskerLeft_F whiskerRight_F
hexagon_reverse 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.hom braiding CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.tensorHom_id hom_ext CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.map_snd_assoc CategoryTheory.Limits.prod.map_fst CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype associator_inv_F CategoryTheory.Category.id_comp braiding_hom_F whiskerRight_F whiskerLeft_F
id_tensorHom_id 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	hom_ext CategoryTheory.Limits.prod.map_id_id CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.prod.map_snd CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.limit.lift_π
leftUnitorImpl_hom_F 📖	mathematical	—	Hom.F tensorObjImpl tensorUnitImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory leftUnitorImpl CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod CategoryTheory.Limits.terminal src tgt CategoryTheory.Limits.terminal.from CategoryTheory.Limits.prod.snd	—	CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.terminal.comp_from CategoryTheory.Category.comp_id
leftUnitorImpl_hom_f 📖	mathematical	—	Hom.f tensorObjImpl tensorUnitImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory leftUnitorImpl CategoryTheory.Limits.prod.snd CategoryTheory.Limits.terminal src	—	—
leftUnitorImpl_inv_F 📖	mathematical	—	Hom.F tensorObjImpl tensorUnitImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory leftUnitorImpl CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod src CategoryTheory.Limits.terminal tgt CategoryTheory.Limits.prod.snd	—	—
leftUnitorImpl_inv_f 📖	mathematical	—	Hom.f tensorObjImpl tensorUnitImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory leftUnitorImpl CategoryTheory.Limits.prod.lift src CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
leftUnitor_hom_F 📖	mathematical	—	Hom.F tensorObjImpl tensorUnitImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.leftUnitor instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod CategoryTheory.Limits.terminal src tgt CategoryTheory.Limits.terminal.from CategoryTheory.Limits.prod.snd	—	CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.terminal.comp_from CategoryTheory.Category.comp_id
leftUnitor_hom_f 📖	mathematical	—	Hom.f tensorObjImpl tensorUnitImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.leftUnitor instMonoidalCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Limits.terminal src	—	—
leftUnitor_inv_F 📖	mathematical	—	Hom.F tensorObjImpl tensorUnitImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.leftUnitor instMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod src CategoryTheory.Limits.terminal tgt CategoryTheory.Limits.prod.snd	—	—
leftUnitor_inv_f 📖	mathematical	—	Hom.f tensorObjImpl tensorUnitImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.leftUnitor instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift src CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
leftUnitor_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	hom_ext CategoryTheory.Limits.prod.map_snd CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype leftUnitor_hom_F CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.terminal.comp_from CategoryTheory.Category.comp_id CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.lift_map_assoc CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.terminal.hom_ext CategoryTheory.Limits.prod.map_fst
pentagon 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.CategoryStruct.id	—	hom_ext CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.map_fst_assoc CategoryTheory.Limits.prod.map_snd CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype associator_hom_F CategoryTheory.Limits.prod.map_snd_assoc CategoryTheory.Category.id_comp
rightUnitorImpl_hom_F 📖	mathematical	—	Hom.F tensorObjImpl tensorUnitImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory rightUnitorImpl CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src CategoryTheory.Limits.terminal tgt CategoryTheory.Limits.prod.snd CategoryTheory.Limits.terminal.from	—	CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.comp_id CategoryTheory.Limits.terminal.comp_from
rightUnitorImpl_hom_f 📖	mathematical	—	Hom.f tensorObjImpl tensorUnitImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory rightUnitorImpl CategoryTheory.Limits.prod.fst src CategoryTheory.Limits.terminal	—	—
rightUnitorImpl_inv_F 📖	mathematical	—	Hom.F tensorObjImpl tensorUnitImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory rightUnitorImpl CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod src tgt CategoryTheory.Limits.terminal CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	—
rightUnitorImpl_inv_f 📖	mathematical	—	Hom.f tensorObjImpl tensorUnitImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory rightUnitorImpl CategoryTheory.Limits.prod.lift src CategoryTheory.Limits.terminal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.terminal.from	—	—
rightUnitor_hom_F 📖	mathematical	—	Hom.F tensorObjImpl tensorUnitImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.rightUnitor instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src CategoryTheory.Limits.terminal tgt CategoryTheory.Limits.prod.snd CategoryTheory.Limits.terminal.from	—	CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.comp_id CategoryTheory.Limits.terminal.comp_from
rightUnitor_hom_f 📖	mathematical	—	Hom.f tensorObjImpl tensorUnitImpl CategoryTheory.Iso.hom CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.rightUnitor instMonoidalCategoryStruct CategoryTheory.Limits.prod.fst src CategoryTheory.Limits.terminal	—	—
rightUnitor_inv_F 📖	mathematical	—	Hom.F tensorObjImpl tensorUnitImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.rightUnitor instMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod src tgt CategoryTheory.Limits.terminal CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst	—	—
rightUnitor_inv_f 📖	mathematical	—	Hom.f tensorObjImpl tensorUnitImpl CategoryTheory.Iso.inv CategoryTheory.Dial instCategory CategoryTheory.MonoidalCategoryStruct.rightUnitor instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift src CategoryTheory.Limits.terminal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.terminal.from	—	—
rightUnitor_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	hom_ext CategoryTheory.Limits.prod.map_fst CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype rightUnitor_hom_F CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.prod.map_snd CategoryTheory.Category.comp_id CategoryTheory.Limits.terminal.comp_from CategoryTheory.Limits.prod.lift_map_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.terminal.hom_ext
symmetry 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.Iso.hom braiding CategoryTheory.CategoryStruct.id	—	hom_ext CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.lift_fst_snd CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype braiding_hom_F CategoryTheory.Limits.prod.map_snd_assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.prod.hom_ext
tensorHomImpl_F 📖	mathematical	—	Hom.F tensorObjImpl tensorHomImpl CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	—
tensorHomImpl_f 📖	mathematical	—	Hom.f tensorObjImpl tensorHomImpl CategoryTheory.Limits.prod.map src	—	—
tensorHom_F 📖	mathematical	—	Hom.F tensorObjImpl CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	—
tensorHom_comp_tensorHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom	—	hom_ext CategoryTheory.Limits.prod.map_map CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.prod.map_map_assoc CategoryTheory.Limits.prod.map_fst CategoryTheory.Category.id_comp CategoryTheory.Limits.prod.map_snd CategoryTheory.Limits.prod.lift_map_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.hom_ext CategoryTheory.Category.assoc CategoryTheory.Category.comp_id
tensorHom_f 📖	mathematical	—	Hom.f tensorObjImpl CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.prod.map src	—	—
tensorObjImpl_rel 📖	mathematical	—	rel tensorObjImpl CategoryTheory.Subobject CategoryTheory.Limits.prod src tgt SemilatticeInf.toMin CategoryTheory.Subobject.semilatticeInf CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	—
tensorObjImpl_src 📖	mathematical	—	src tensorObjImpl CategoryTheory.Limits.prod	—	—
tensorObjImpl_tgt 📖	mathematical	—	tgt tensorObjImpl CategoryTheory.Limits.prod	—	—
tensorObj_rel 📖	mathematical	—	rel CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Subobject CategoryTheory.Limits.prod src tgt SemilatticeInf.toMin CategoryTheory.Subobject.semilatticeInf CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	—
tensorObj_src 📖	mathematical	—	src CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.prod	—	—
tensorObj_tgt 📖	mathematical	—	tgt CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.prod	—	—
tensorUnitImpl_rel 📖	mathematical	—	rel tensorUnitImpl Top.top CategoryTheory.Subobject CategoryTheory.Limits.prod CategoryTheory.Limits.terminal OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.orderTop	—	—
tensorUnitImpl_src 📖	mathematical	—	src tensorUnitImpl CategoryTheory.Limits.terminal	—	—
tensorUnitImpl_tgt 📖	mathematical	—	tgt tensorUnitImpl CategoryTheory.Limits.terminal	—	—
tensorUnit_rel 📖	mathematical	—	rel CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Dial instCategory instMonoidalCategoryStruct Top.top CategoryTheory.Subobject CategoryTheory.Limits.prod CategoryTheory.Limits.terminal OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.orderTop	—	—
tensorUnit_src 📖	mathematical	—	src CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.terminal	—	—
tensorUnit_tgt 📖	mathematical	—	tgt CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.terminal	—	—
triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	hom_ext CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.comp_id CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.prod.map_fst CategoryTheory.Limits.prod.map_snd CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype leftUnitor_hom_F CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.terminal.comp_from CategoryTheory.Limits.prod.map_snd_assoc CategoryTheory.Category.id_comp associator_hom_F CategoryTheory.Limits.limit.lift_π_assoc rightUnitor_hom_F
whiskerLeft_F 📖	mathematical	—	Hom.F tensorObjImpl CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.map	—	CategoryTheory.Limits.prod.map_snd
whiskerLeft_f 📖	mathematical	—	Hom.f tensorObjImpl CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.prod.map src CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
whiskerRight_F 📖	mathematical	—	Hom.F tensorObjImpl CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod src tgt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	CategoryTheory.Limits.prod.map_snd
whiskerRight_f 📖	mathematical	—	Hom.f tensorObjImpl CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Dial instCategory instMonoidalCategoryStruct CategoryTheory.Limits.prod.map src CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

---

← Back to Index