Documentation Verification Report

Braiding

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

Statistics

Metric	Count
Definitions `braiding`, `braidedCategory`, `symmetricCategory`	3
Theorems `braiding_naturality_left`, `braiding_naturality_right`, `hexagon_forward`, `hexagon_reverse`, `symmetry`, `symmetry_assoc`	6
Total	9

CategoryTheory.GradedObject

Definitions

Name	Category	Theorems
`braidedCategory` 📖	CompOp	—
`symmetricCategory` 📖	CompOp	—

CategoryTheory.GradedObject.Monoidal

Definitions

Name	Category	Theorems
`braiding` 📖	CompOp	6 math math: `symmetry`, `symmetry_assoc`, `hexagon_reverse`, `braiding_naturality_left`, `braiding_naturality_right`, `hexagon_forward`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`braiding_naturality_left` 📖	mathematical	`CategoryTheory.GradedObject.HasTensor` `AddCommMonoid.toAddMonoid`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.GradedObject` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.GradedObject.categoryOfGradedObjects` `tensorObj` `whiskerRight` `CategoryTheory.Iso.hom` `braiding` `whiskerLeft`	—	`CategoryTheory.GradedObject.hom_ext` `tensorObj_ext` `ι_tensorHom_assoc` `CategoryTheory.MonoidalCategory.tensorHom_id` `ι_tensorObjDesc` `CategoryTheory.BraidedCategory.braiding_naturality_left_assoc` `ι_tensorObjDesc_assoc` `CategoryTheory.Category.assoc` `ι_tensorHom` `CategoryTheory.MonoidalCategory.id_tensorHom`
`braiding_naturality_right` 📖	mathematical	`CategoryTheory.GradedObject.HasTensor` `AddCommMonoid.toAddMonoid`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.GradedObject` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.GradedObject.categoryOfGradedObjects` `tensorObj` `whiskerLeft` `CategoryTheory.Iso.hom` `braiding` `whiskerRight`	—	`CategoryTheory.GradedObject.hom_ext` `tensorObj_ext` `ι_tensorHom_assoc` `CategoryTheory.MonoidalCategory.id_tensorHom` `ι_tensorObjDesc` `CategoryTheory.BraidedCategory.braiding_naturality_right_assoc` `ι_tensorObjDesc_assoc` `CategoryTheory.Category.assoc` `ι_tensorHom` `CategoryTheory.MonoidalCategory.tensorHom_id`
`hexagon_forward` 📖	mathematical	`CategoryTheory.GradedObject.HasTensor` `AddCommMonoid.toAddMonoid` `tensorObj` `CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor` `CategoryTheory.GradedObject.HasGoodTensorTensor₂₃`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.GradedObject` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.GradedObject.categoryOfGradedObjects` `CategoryTheory.Iso.hom` `associator` `braiding` `whiskerRight` `whiskerLeft`	—	`CategoryTheory.GradedObject.hom_ext` `tensorObj₃'_ext` `add_comm` `add_assoc` `ιTensorObj₃'_associator_hom_assoc` `ιTensorObj₃_eq` `CategoryTheory.Category.assoc` `ι_tensorObjDesc_assoc` `CategoryTheory.MonoidalCategory.id_tensorHom` `CategoryTheory.BraidedCategory.braiding_naturality_assoc` `CategoryTheory.BraidedCategory.braiding_tensor_right_hom` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.MonoidalCategory.tensorHom_id` `ιTensorObj₃'_eq_assoc` `ιTensorObj₃'_associator_hom` `CategoryTheory.Iso.inv_hom_id_assoc` `ιTensorObj₃'_eq` `ι_tensorHom_assoc` `CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc` `CategoryTheory.Category.id_comp` `ι_tensorObjDesc` `CategoryTheory.GradedObject.categoryOfGradedObjects_id` `CategoryTheory.MonoidalCategory.comp_tensor_id` `ι_tensorHom` `CategoryTheory.MonoidalCategory.id_tensor_comp_assoc` `CategoryTheory.MonoidalCategory.id_tensor_comp` `CategoryTheory.MonoidalCategory.whiskerLeft_comp`
`hexagon_reverse` 📖	mathematical	`CategoryTheory.GradedObject.HasTensor` `AddCommMonoid.toAddMonoid` `tensorObj` `CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor` `CategoryTheory.GradedObject.HasGoodTensorTensor₂₃`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.GradedObject` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.GradedObject.categoryOfGradedObjects` `CategoryTheory.Iso.inv` `associator` `CategoryTheory.Iso.hom` `braiding` `whiskerLeft` `whiskerRight`	—	`CategoryTheory.GradedObject.hom_ext` `tensorObj₃_ext` `add_assoc` `add_comm` `ιTensorObj₃_associator_inv_assoc` `ιTensorObj₃'_eq` `CategoryTheory.Category.assoc` `ι_tensorObjDesc_assoc` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.BraidedCategory.braiding_naturality_assoc` `CategoryTheory.BraidedCategory.braiding_tensor_left_hom` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.MonoidalCategory.id_tensorHom` `ιTensorObj₃_eq_assoc` `ιTensorObj₃_associator_inv` `CategoryTheory.Iso.hom_inv_id_assoc` `ιTensorObj₃_eq` `ι_tensorHom_assoc` `CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc` `CategoryTheory.Category.id_comp` `ι_tensorObjDesc` `CategoryTheory.GradedObject.categoryOfGradedObjects_id` `CategoryTheory.MonoidalCategory.id_tensor_comp` `ι_tensorHom` `CategoryTheory.MonoidalCategory.comp_tensor_id_assoc` `CategoryTheory.MonoidalCategory.comp_tensor_id`
`symmetry` 📖	mathematical	`CategoryTheory.GradedObject.HasTensor` `AddCommMonoid.toAddMonoid`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.GradedObject` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.GradedObject.categoryOfGradedObjects` `tensorObj` `CategoryTheory.Iso.hom` `braiding` `CategoryTheory.SymmetricCategory.toBraidedCategory` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.GradedObject.hom_ext` `tensorObj_ext` `ι_tensorObjDesc_assoc` `CategoryTheory.Category.assoc` `ι_tensorObjDesc` `CategoryTheory.SymmetricCategory.symmetry_assoc` `CategoryTheory.Category.comp_id`
`symmetry_assoc` 📖	mathematical	`CategoryTheory.GradedObject.HasTensor` `AddCommMonoid.toAddMonoid`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.GradedObject` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.GradedObject.categoryOfGradedObjects` `tensorObj` `CategoryTheory.Iso.hom` `braiding` `CategoryTheory.SymmetricCategory.toBraidedCategory`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `symmetry`

---

← Back to Index