Opposite

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

Statistics

Metric	Count
Definitions instBraidedCategoryOpposite	1
Theorems op_tensorμ, unop_tensorμ	2
Total	3

CategoryTheory.BraidedCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_tensorμ 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorμ Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp instBraidedCategoryOpposite Opposite.op	—	CategoryTheory.Category.assoc
unop_tensorμ 📖	mathematical	—	Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp CategoryTheory.MonoidalCategory.tensorμ instBraidedCategoryOpposite Opposite.unop	—	CategoryTheory.Category.assoc

(root)

Definitions

Name	Category	Theorems
instBraidedCategoryOpposite 📖	CompOp	16 math math: CategoryTheory.Comon.tensorObj_comul', CategoryTheory.Comon.monoidal_rightUnitor_inv_hom, CategoryTheory.BraidedCategory.unop_tensorμ, CategoryTheory.Comon.monoidal_whiskerLeft_hom, CategoryTheory.Comon.monoidal_leftUnitor_hom_hom, CategoryTheory.Comon.monoidal_whiskerRight_hom, CategoryTheory.Comon.monoidal_associator_hom_hom, CategoryTheory.Comon.monoidal_tensorUnit_comon_comul, CategoryTheory.Comon.monoidal_leftUnitor_inv_hom, CategoryTheory.Comon.monoidal_rightUnitor_hom_hom, CategoryTheory.BraidedCategory.op_tensorμ, CategoryTheory.Comon.monoidal_associator_inv_hom, CategoryTheory.Comon.monoidal_tensorUnit_comon_counit, CategoryTheory.Comon.monoidal_tensorHom_hom, CategoryTheory.Comon.monoidal_tensorObj_comon_counit, CategoryTheory.Comon.monoidal_tensorObj_comon_comul

---

← Back to Index