The monoidal category structure on R-modules
Mostly this uses existing machinery in linear_algebra.tensor_product.
We just need to provide a few small missing pieces to build the
monoidal_category instance.
If you're happy using the bundled Module 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
- Module.monoidal_category.tensor_obj M N = Module.of R (tensor_product R ↥M ↥N)
def
Module.monoidal_category.tensor_hom
{R : Type u}
[comm_ring R]
{M N M' N' : Module R} :
(M ⟶ N) → (M' ⟶ N') → (Module.monoidal_category.tensor_obj M M' ⟶ Module.monoidal_category.tensor_obj N N')
(implementation) tensor product of morphisms R-modules
Equations
theorem
Module.monoidal_category.tensor_id
{R : Type u}
[comm_ring R]
(M N : Module R) :
Module.monoidal_category.tensor_hom (𝟙 M) (𝟙 N) = 𝟙 (Module.of R (tensor_product R ↥M ↥N))
theorem
Module.monoidal_category.tensor_comp
{R : Type u}
[comm_ring R]
{X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Module R}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₂)
(g₁ : Y₁ ⟶ Z₁)
(g₂ : Y₂ ⟶ Z₂) :
Module.monoidal_category.tensor_hom (f₁ ≫ g₁) (f₂ ≫ g₂) = Module.monoidal_category.tensor_hom f₁ f₂ ≫ Module.monoidal_category.tensor_hom g₁ g₂
(implementation) the associator for R-modules
Equations
- Module.monoidal_category.associator M N K = (tensor_product.assoc R ↥M ↥N ↥K).to_Module_iso
theorem
Module.monoidal_category.pentagon
{R : Type u}
[comm_ring R]
(W X Y Z : Module R) :
Module.monoidal_category.tensor_hom (Module.monoidal_category.associator W X Y).hom (𝟙 Z) ≫ (Module.monoidal_category.associator W (Module.monoidal_category.tensor_obj X Y) Z).hom ≫ Module.monoidal_category.tensor_hom (𝟙 W) (Module.monoidal_category.associator X Y Z).hom = (Module.monoidal_category.associator (Module.monoidal_category.tensor_obj W X) Y Z).hom ≫ (Module.monoidal_category.associator W X (Module.monoidal_category.tensor_obj Y Z)).hom
def
Module.monoidal_category.left_unitor
{R : Type u}
[comm_ring R]
(M : Module R) :
Module.of R (tensor_product R R ↥M) ≅ M
(implementation) the left unitor for R-modules
Equations
theorem
Module.monoidal_category.left_unitor_naturality
{R : Type u}
[comm_ring R]
{M N : Module R}
(f : M ⟶ N) :
def
Module.monoidal_category.right_unitor
{R : Type u}
[comm_ring R]
(M : Module R) :
Module.of R (tensor_product R ↥M R) ≅ M
(implementation) the right unitor for R-modules
Equations
theorem
Module.monoidal_category.right_unitor_naturality
{R : Type u}
[comm_ring R]
{M N : Module R}
(f : M ⟶ N) :
@[instance]
Equations
- Module.Module.monoidal_category = {tensor_obj := Module.monoidal_category.tensor_obj _inst_1, tensor_hom := Module.monoidal_category.tensor_hom _inst_1, tensor_id' := _, tensor_comp' := _, tensor_unit := Module.of R R semiring.to_semimodule, associator := Module.monoidal_category.associator _inst_1, associator_naturality' := _, left_unitor := Module.monoidal_category.left_unitor _inst_1, left_unitor_naturality' := _, right_unitor := Module.monoidal_category.right_unitor _inst_1, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
@[instance]
Remind ourselves that the monoidal unit, being just R, is still a commutative ring.
Equations
- Module.comm_ring = _inst_1