The monoidal category structure on R-modules #
Mostly this uses existing machinery in LinearAlgebra.TensorProduct
.
We just need to provide a few small missing pieces to build the
MonoidalCategory
instance.
The SymmetricCategory
instance is in Algebra.Category.ModuleCat.Monoidal.Symmetric
to reduce imports.
Note the universe level of the modules must be at least the universe level of the ring, so that we have a monoidal unit. For now, we simplify by insisting both universe levels are the same.
We construct the monoidal closed structure on ModuleCat R
in
Algebra.Category.ModuleCat.Monoidal.Closed
.
If you're happy using the bundled ModuleCat R
, it may be possible to mostly
use this as an interface and not need to interact much with the implementation details.
(implementation) tensor product of R-modules
Equations
- ModuleCat.MonoidalCategory.tensorObj M N = ModuleCat.of R (TensorProduct R ↑M ↑N)
Instances For
(implementation) tensor product of morphisms R-modules
Equations
- ModuleCat.MonoidalCategory.tensorHom f g = ModuleCat.ofHom (TensorProduct.map f.hom g.hom)
Instances For
(implementation) left whiskering for R-modules
Equations
- ModuleCat.MonoidalCategory.whiskerLeft M f = ModuleCat.ofHom (LinearMap.lTensor (↑M) f.hom)
Instances For
(implementation) right whiskering for R-modules
Equations
- ModuleCat.MonoidalCategory.whiskerRight f N = ModuleCat.ofHom (LinearMap.rTensor (↑N) f.hom)
Instances For
(implementation) the associator for R-modules
Equations
- ModuleCat.MonoidalCategory.associator M N K = (TensorProduct.assoc R ↑M ↑N ↑K).toModuleIso
Instances For
(implementation) the left unitor for R-modules
Equations
- ModuleCat.MonoidalCategory.leftUnitor M = (TensorProduct.lid R ↑M).toModuleIso ≪≫ M.ofSelfIso
Instances For
(implementation) the right unitor for R-modules
Equations
- ModuleCat.MonoidalCategory.rightUnitor M = (TensorProduct.rid R ↑M).toModuleIso ≪≫ M.ofSelfIso
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- ModuleCat.monoidalCategory = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Remind ourselves that the monoidal unit, being just R
, is still a commutative ring.
Equations
- ModuleCat.instCommRingCarrierTensorUnit = inferInstanceAs (CommRing R)
Construct for morphisms from the tensor product of two objects in ModuleCat
.
Equations
- ModuleCat.MonoidalCategory.tensorLift f h₁ h₂ h₃ h₄ = ModuleCat.ofHom (TensorProduct.lift (LinearMap.mk₂ R f h₁ h₂ h₃ h₄))
Instances For
Extensionality lemma for morphisms from a module of the form (M₁ ⊗ M₂) ⊗ M₃
.
Extensionality lemma for morphisms from a module of the form M₁ ⊗ (M₂ ⊗ M₃)
.