Braided

📁 Source: Mathlib/CategoryTheory/Monoidal/DayConvolution/Braided.lean

Statistics

Metric	Count
Definitions braiding, braidingHomCorepresenting, braidingInvCorepresenting	3
Theorems braidingHomCorepresenting_app, braidingInvCorepresenting_app, braiding_naturality_left, braiding_naturality_left_assoc, braiding_naturality_right, braiding_naturality_right_assoc, hexagon_forward, hexagon_reverse, symmetry, unit_app_braiding_hom_app, unit_app_braiding_hom_app_assoc, unit_app_braiding_inv_app, unit_app_braiding_inv_app_assoc	13
Total	16

CategoryTheory.MonoidalCategory.DayConvolution

Definitions

Name	Category	Theorems
braiding 📖	CompOp	11 math math: braiding_naturality_left_assoc, hexagon_forward, hexagon_reverse, braiding_naturality_right, braiding_naturality_right_assoc, unit_app_braiding_inv_app, symmetry, unit_app_braiding_hom_app, unit_app_braiding_hom_app_assoc, unit_app_braiding_inv_app_assoc, braiding_naturality_left
braidingHomCorepresenting 📖	CompOp	1 math math: braidingHomCorepresenting_app
braidingInvCorepresenting 📖	CompOp	1 math math: braidingInvCorepresenting_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
braidingHomCorepresenting_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution braidingHomCorepresenting CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding unit CategoryTheory.Functor.map	—	—
braidingInvCorepresenting_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution braidingInvCorepresenting CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding unit CategoryTheory.Functor.map	—	—
braiding_naturality_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom braiding	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension leftKanExtension CategoryTheory.NatTrans.ext' unit_app_map_app_assoc CategoryTheory.MonoidalCategory.tensorHom_id unit_app_braiding_hom_app CategoryTheory.BraidedCategory.braiding_naturality_left_assoc unit_app_braiding_hom_app_assoc CategoryTheory.NatTrans.naturality CategoryTheory.MonoidalCategory.id_tensorHom
braiding_naturality_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom braiding	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' braiding_naturality_left
braiding_naturality_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom braiding	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension leftKanExtension CategoryTheory.NatTrans.ext' unit_app_map_app_assoc CategoryTheory.MonoidalCategory.id_tensorHom unit_app_braiding_hom_app CategoryTheory.BraidedCategory.braiding_naturality_right_assoc unit_app_braiding_hom_app_assoc CategoryTheory.NatTrans.naturality CategoryTheory.MonoidalCategory.tensorHom_id
braiding_naturality_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom braiding	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' braiding_naturality_right
hexagon_forward 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution CategoryTheory.Iso.hom associator braiding map CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension leftKanExtension instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id associator_hom_unit_unit_assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.NatTrans.naturality unit_app_braiding_hom_app_assoc CategoryTheory.BraidedCategory.braiding_tensor_left_hom CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Iso.map_hom_inv_id CategoryTheory.BraidedCategory.braiding_naturality_right_assoc CategoryTheory.BraidedCategory.braiding_tensor_right_hom CategoryTheory.Iso.map_inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.hom_inv_id_assoc unit_app_map_app_assoc CategoryTheory.MonoidalCategory.tensorHom_id unit_app_braiding_hom_app CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.comp_whiskerRight whiskerRight_comp_unit_app_assoc CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.BraidedCategory.hexagon_reverse CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc CategoryTheory.eq_whisker CategoryTheory.Iso.hom_inv_id whiskerLeft_comp_unit_app_assoc CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc
hexagon_reverse 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution CategoryTheory.Iso.inv associator CategoryTheory.Iso.hom braiding map CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension leftKanExtension instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id associator_inv_unit_unit_assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.NatTrans.naturality unit_app_braiding_hom_app_assoc CategoryTheory.BraidedCategory.braiding_tensor_right_hom CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Iso.map_inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.BraidedCategory.braiding_naturality_left_assoc CategoryTheory.BraidedCategory.braiding_tensor_left_hom CategoryTheory.Iso.map_hom_inv_id_assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Iso.inv_hom_id_assoc unit_app_map_app_assoc CategoryTheory.MonoidalCategory.id_tensorHom unit_app_braiding_hom_app CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whiskerLeft_comp whiskerLeft_comp_unit_app_assoc CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.BraidedCategory.hexagon_forward CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc CategoryTheory.Iso.map_hom_inv_id CategoryTheory.eq_whisker whiskerRight_comp_unit_app_assoc CategoryTheory.MonoidalCategory.inv_hom_whiskerRight_assoc
symmetry 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution CategoryTheory.Iso.hom braiding CategoryTheory.SymmetricCategory.toBraidedCategory CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension leftKanExtension CategoryTheory.NatTrans.ext' unit_app_braiding_hom_app_assoc CategoryTheory.NatTrans.naturality CategoryTheory.SymmetricCategory.symmetry CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.SymmetricCategory.symmetry_assoc
unit_app_braiding_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app unit CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category braiding CategoryTheory.BraidedCategory.braiding CategoryTheory.Functor.map	—	CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app leftKanExtension
unit_app_braiding_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct convolution CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp unit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category braiding CategoryTheory.BraidedCategory.braiding CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_app_braiding_hom_app
unit_app_braiding_inv_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app unit CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category braiding CategoryTheory.BraidedCategory.braiding CategoryTheory.Functor.map	—	CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app leftKanExtension
unit_app_braiding_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct convolution CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp unit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category braiding CategoryTheory.BraidedCategory.braiding CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_app_braiding_inv_app

---

← Back to Index