Symmetric

📁 Source: Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

Statistics

Metric	Count
Definitions instBraidedCategory, instBraidedSemimoduleCatFunctorEquivalenceSemimoduleCat, symmetricCategory, symmetricCategory, braiding	5
Theorems braiding_hom_apply, braiding_inv_apply, tensorμ_apply, tensorμ_eq_tensorTensorTensorComm, braiding_hom_apply, braiding_inv_apply, braiding_naturality, braiding_naturality_left, braiding_naturality_right, hexagon_forward, hexagon_reverse, tensorμ_apply, tensorμ_eq_tensorTensorTensorComm	13
Total	18

ModuleCat.MonoidalCategory

Definitions

Name	Category	Theorems
instBraidedCategory 📖	CompOp	4 math math: braiding_hom_apply, tensorμ_eq_tensorTensorTensorComm, tensorμ_apply, braiding_inv_apply
instBraidedSemimoduleCatFunctorEquivalenceSemimoduleCat 📖	CompOp	—
symmetricCategory 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
braiding_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ModuleCat.monoidalCategory ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding instBraidedCategory TensorProduct.tmul CommRing.toCommSemiring	—	—
braiding_inv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ModuleCat.monoidalCategory ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding instBraidedCategory TensorProduct.tmul CommRing.toCommSemiring	—	—
tensorμ_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ModuleCat.monoidalCategory ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.MonoidalCategory.tensorμ instBraidedCategory TensorProduct.tmul CommRing.toCommSemiring TensorProduct TensorProduct.addCommMonoid	—	—
tensorμ_eq_tensorTensorTensorComm 📖	mathematical	—	CategoryTheory.MonoidalCategory.tensorμ ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory instBraidedCategory ModuleCat.ofHom TensorProduct CommRing.toCommSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.addCommGroup LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct.tensorTensorTensorComm	—	ModuleCat.hom_ext RingHomInvPair.ids TensorProduct.ext smulCommClass_self RingHomCompTriple.ids LinearMap.ext₂

SemimoduleCat

Definitions

Name	Category	Theorems
braiding 📖	CompOp	5 math math: MonoidalCategory.braiding_naturality_right, MonoidalCategory.hexagon_forward, MonoidalCategory.braiding_naturality, MonoidalCategory.hexagon_reverse, MonoidalCategory.braiding_naturality_left

SemimoduleCat.MonoidalCategory

Definitions

Name	Category	Theorems
symmetricCategory 📖	CompOp	4 math math: tensorμ_apply, braiding_hom_apply, braiding_inv_apply, tensorμ_eq_tensorTensorTensorComm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
braiding_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj SemimoduleCat CommSemiring.toSemiring SemimoduleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct SemimoduleCat.monoidalCategory SemimoduleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule LinearMap.instFunLike SemimoduleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.SymmetricCategory.toBraidedCategory symmetricCategory TensorProduct.tmul	—	—
braiding_inv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj SemimoduleCat CommSemiring.toSemiring SemimoduleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct SemimoduleCat.monoidalCategory SemimoduleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule LinearMap.instFunLike SemimoduleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding CategoryTheory.SymmetricCategory.toBraidedCategory symmetricCategory TensorProduct.tmul	—	—
braiding_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SemimoduleCat CommSemiring.toSemiring CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom SemimoduleCat.braiding	—	SemimoduleCat.hom_ext TensorProduct.ext'
braiding_naturality_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SemimoduleCat CommSemiring.toSemiring CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom SemimoduleCat.braiding CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	braiding_naturality
braiding_naturality_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SemimoduleCat CommSemiring.toSemiring CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom SemimoduleCat.braiding CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	braiding_naturality
hexagon_forward 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SemimoduleCat CommSemiring.toSemiring CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator SemimoduleCat.braiding CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	SemimoduleCat.hom_ext TensorProduct.ext_threefold
hexagon_reverse 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SemimoduleCat CommSemiring.toSemiring CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.hom SemimoduleCat.braiding CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom SemimoduleCat.hom_ext TensorProduct.ext_threefold
tensorμ_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj SemimoduleCat CommSemiring.toSemiring SemimoduleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct SemimoduleCat.monoidalCategory SemimoduleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule LinearMap.instFunLike SemimoduleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.SymmetricCategory.toBraidedCategory symmetricCategory TensorProduct.tmul TensorProduct TensorProduct.addCommMonoid	—	—
tensorμ_eq_tensorTensorTensorComm 📖	mathematical	—	CategoryTheory.MonoidalCategory.tensorμ SemimoduleCat CommSemiring.toSemiring SemimoduleCat.moduleCategory SemimoduleCat.monoidalCategory CategoryTheory.SymmetricCategory.toBraidedCategory symmetricCategory SemimoduleCat.ofHom TensorProduct SemimoduleCat.carrier SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule TensorProduct.addCommMonoid TensorProduct.instModule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct.tensorTensorTensorComm	—	SemimoduleCat.hom_ext RingHomInvPair.ids TensorProduct.ext smulCommClass_self RingHomCompTriple.ids LinearMap.ext₂

---

← Back to Index