Braided

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

Statistics

Metric	Count
Definitions braidingNatIso, instBraidedCategoryLocalizedMonoidal, instBraidedLocalizedMonoidalToMonoidalCategory, instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorFlipCurriedTensorObjWhiskeringRightTensorBifunctor, instSymmetricCategoryLocalizedMonoidal	5
Theorems braidingNatIso_hom_app, braidingNatIso_hom_app_naturality_μ_left, braidingNatIso_hom_app_naturality_μ_left_assoc, braidingNatIso_hom_app_naturality_μ_right, braidingNatIso_hom_app_naturality_μ_right_assoc, instIsLocalizationLocalizedMonoidalToMonoidalCategory_1, map_hexagon_forward, map_hexagon_forward_assoc, map_hexagon_reverse, map_hexagon_reverse_assoc, β_hom_app	11
Total	16

CategoryTheory.Localization.Monoidal

Definitions

Name	Category	Theorems
braidingNatIso 📖	CompOp	9 math math: map_hexagon_forward, map_hexagon_reverse, map_hexagon_reverse_assoc, braidingNatIso_hom_app_naturality_μ_left_assoc, braidingNatIso_hom_app, braidingNatIso_hom_app_naturality_μ_left, map_hexagon_forward_assoc, braidingNatIso_hom_app_naturality_μ_right, braidingNatIso_hom_app_naturality_μ_right_assoc
instBraidedCategoryLocalizedMonoidal 📖	CompOp	1 math math: β_hom_app
instBraidedLocalizedMonoidalToMonoidalCategory 📖	CompOp	—
instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorFlipCurriedTensorObjWhiskeringRightTensorBifunctor 📖	CompOp	—
instSymmetricCategoryLocalizedMonoidal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
braidingNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensorBifunctor toMonoidalCategory CategoryTheory.Functor.flip CategoryTheory.Iso.hom braidingNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategoryLocalizedMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory CategoryTheory.Functor.map CategoryTheory.BraidedCategory.braiding CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	leftUnitor_hom_app rightUnitor_hom_app CategoryTheory.Localization.lift₂NatTrans_app_app instIsLocalizationLocalizedMonoidalToMonoidalCategory_1
braidingNatIso_hom_app_naturality_μ_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensorBifunctor toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.hom braidingNatIso CategoryTheory.MonoidalCategoryStruct.whiskerRight instMonoidalCategoryLocalizedMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.NatTrans.naturality
braidingNatIso_hom_app_naturality_μ_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensorBifunctor toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.flip CategoryTheory.NatTrans.app CategoryTheory.Iso.hom braidingNatIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight instMonoidalCategoryLocalizedMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' braidingNatIso_hom_app_naturality_μ_left
braidingNatIso_hom_app_naturality_μ_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensorBifunctor CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct toMonoidalCategory CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.hom braidingNatIso CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.μ instMonoidalCategoryLocalizedMonoidal CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.NatTrans.congr_app CategoryTheory.NatTrans.naturality
braidingNatIso_hom_app_naturality_μ_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensorBifunctor CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct toMonoidalCategory CategoryTheory.Functor.flip CategoryTheory.NatTrans.app CategoryTheory.Iso.hom braidingNatIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.μ instMonoidalCategoryLocalizedMonoidal CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' braidingNatIso_hom_app_naturality_μ_right
instIsLocalizationLocalizedMonoidalToMonoidalCategory_1 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal toMonoidalCategory	—	—
map_hexagon_forward 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip tensorBifunctor CategoryTheory.Iso.app braidingNatIso CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.associator_hom braidingNatIso_hom_app leftUnitor_hom_app rightUnitor_hom_app CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc CategoryTheory.Functor.LaxMonoidal.μ_natural_left braidingNatIso_hom_app_naturality_μ_left CategoryTheory.BraidedCategory.braiding_tensor_right_hom CategoryTheory.Functor.map_comp CategoryTheory.Functor.LaxMonoidal.associativity_inv_assoc CategoryTheory.Functor.Monoidal.δ_μ CategoryTheory.Category.comp_id CategoryTheory.Iso.map_inv_hom_id CategoryTheory.Functor.OplaxMonoidal.associativity_inv_assoc CategoryTheory.Functor.Monoidal.δ_μ_assoc CategoryTheory.Iso.map_hom_inv_id_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc
map_hexagon_forward_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip tensorBifunctor CategoryTheory.Iso.app braidingNatIso CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_hexagon_forward
map_hexagon_reverse 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip tensorBifunctor CategoryTheory.Iso.hom CategoryTheory.Iso.app braidingNatIso CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.associator_inv braidingNatIso_hom_app leftUnitor_hom_app rightUnitor_hom_app CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp braidingNatIso_hom_app_naturality_μ_right CategoryTheory.BraidedCategory.braiding_tensor_left_hom CategoryTheory.Functor.map_comp CategoryTheory.Functor.LaxMonoidal.associativity_assoc CategoryTheory.Functor.Monoidal.δ_μ CategoryTheory.Category.comp_id CategoryTheory.Iso.map_hom_inv_id CategoryTheory.Functor.OplaxMonoidal.associativity_assoc CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc CategoryTheory.Functor.Monoidal.δ_μ_assoc CategoryTheory.Iso.map_inv_hom_id_assoc CategoryTheory.Functor.LaxMonoidal.μ_natural_right CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc
map_hexagon_reverse_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip tensorBifunctor CategoryTheory.Iso.hom CategoryTheory.Iso.app braidingNatIso CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_hexagon_reverse
β_hom_app 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategoryLocalizedMonoidal CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.BraidedCategory.braiding instBraidedCategoryLocalizedMonoidal CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	braidingNatIso_hom_app

---

← Back to Index