Structures · Category theory
CategoryTheory.SymmetricCategory
A symmetric monoidal category is a braided monoidal category for which the braiding is symmetric.
- Shape
- One type argument · adds symmetry
Extends1
Extended by1
Concrete types that are instances18
- CategoryTheory.Functor
- ModuleCat
- Action
- CategoryTheory.Mon
- CategoryTheory.ObjectProperty.FullSubcategory
- Rep
- PresheafOfModules
- AlgCat
- CategoryTheory.GradedObject
- CategoryTheory.AddMon
- QuadraticModuleCat
- SemimoduleCat
- CategoryTheory.Monoidal.Transported
- CategoryTheory.WideSubcategory
- CategoryTheory.Dial
- CategoryTheory.LocalizedMonoidal
- LightCondMod
- SFinKer
How is a type an instance?
Loading the hierarchy index…
Assumed by47
- CategoryTheory.SymmetricCategory.symmetry_assoc
- CategoryTheory.SymmetricCategory.symmetry
- CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding
- CategoryTheory.SymmetricCategory.tensorμ_braid_swap
- CategoryTheory.GradedObject.Monoidal.symmetry
- CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib
- CategoryTheory.Functor.instBraidedMonMapMon
- CategoryTheory.Monoidal.functorCategorySymmetric
- CategoryTheory.Sheaf.symmetricCategory
- CategoryTheory.Pi.symmetricCategory
- CategoryTheory.MonObj.mul_braiding
- CategoryTheory.AddMon.braiding_hom_hom
- CategoryTheory.SymmetricCategory.toBraidedCategory
- CategoryTheory.AddMon.instSymmetricCategory
- CategoryTheory.Mon.braiding_hom_hom
- CategoryTheory.ObjectProperty.fullSymmetricSubcategory
- CategoryTheory.Mon.instSymmetricCategory
- CategoryTheory.Functor.instLaxBraidedMonMapAddMon
- CategoryTheory.Mon.braiding_inv_hom
- CategoryTheory.SymmetricCategory.equivReverseBraiding
- CategoryTheory.Monoidal.Transported.instSymmetricCategory
- CategoryTheory.GradedObject.symmetricCategory
- CategoryTheory.Monoidal.Reflective.isIso_tfae
- Action.instSymmetricCategory
- CategoryTheory.MonObj.instIsMonHomHomBraiding
- CategoryTheory.Monoidal.Reflective.monoidalClosed
- CategoryTheory.Monoidal.Reflective.instIsIsoAppUnitObjIhom
- CategoryTheory.AddMonObj.add_braiding
- CategoryTheory.Functor.instBraidedMonMapAddMon
- CategoryTheory.AddMon.braiding_neg_hom
- CategoryTheory.SymmetricCategory.tensorμ_braid_swap_assoc
- CategoryTheory.isMonoidalDistrib.of_symmetric_monoidal_closed
- CategoryTheory.WideSubcategory.instSymmetricCategory
- CategoryTheory.instIsCommAddMonObjTensorObj
- CategoryTheory.SymmetricCategory.ofFaithful
- CategoryTheory.coprodComparison_tensorRight_braiding_hom
- CategoryTheory.SymmetricCategory.rightDistrib_of_leftDistrib
- CategoryTheory.SymmetricCategory.ofFullyFaithful
- CategoryTheory.instIsCommComonObjTensorObj
- CategoryTheory.AddMonObj.instIsAddMonHomHomBraiding
- CategoryTheory.MonoidalCategory.DayConvolution.symmetry
- CategoryTheory.SymmetricCategory.reverseBraiding_eq
- CategoryTheory.Localization.Monoidal.instSymmetricCategoryLocalizedMonoidal
- CategoryTheory.Monoidal.Reflective.closed
- CategoryTheory.Functor.instLaxBraidedMonMapMon
- CategoryTheory.GradedObject.Monoidal.symmetry_assoc
- CategoryTheory.instIsCommMonObjTensorObj