Theorems · Definition · category theory
SemimoduleCat.braiding
{R : Type u} →
[inst : CommSemiring R] →
(M N : SemimoduleCat R) →
CategoryTheory.MonoidalCategoryStruct.tensorObj M N ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj N M(implementation) the braiding for R-modules
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- CategoryTheory.Isostatement · cited by 3,963
- CategoryTheory.MonoidalCategoryStruct.tensorObjstatement · cited by 3,106
- SemimoduleCatstatement and proof · cited by 108
- TensorProduct.commproof · cited by 108
- SemimoduleCat.carrierproof · cited by 87
- LinearEquiv.toModuleIsoₛproof · cited by 7
Cited by5
Results whose statement or proof uses this declaration.
- SemimoduleCat.MonoidalCategory.braiding_naturalitystatement and proof · cited by 2
- SemimoduleCat.MonoidalCategory.braiding_naturality_leftstatement and proof · cited by 0
- SemimoduleCat.MonoidalCategory.braiding_naturality_rightstatement and proof · cited by 0
- SemimoduleCat.MonoidalCategory.hexagon_forwardstatement and proof · cited by 0
- SemimoduleCat.MonoidalCategory.hexagon_reversestatement and proof · cited by 0