English
The category ModuleCat R is equipped with a MonoidalLinear structure over R; i.e., the tensor operation is bilinear in each argument, compatible with the module structure.
Русский
Категория ModuleCat R оснащена структурой MonoidalLinear над R; тензорная операция билинеарна по каждому аргументу и совместима с модульной структурой.
LaTeX
$$$\\text{MonoidalLinear}_R(\\text{ModuleCat } R)$$$
Lean4
/-- Auxiliary definition for the `MonoidalClosed` instance on `Module R`.
(This is only a separate definition in order to speed up typechecking.)
-/
def monoidalClosedHomEquiv (M N P : ModuleCat.{u} R) :
((MonoidalCategory.tensorLeft M).obj N ⟶ P) ≃ (N ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj P)
where
toFun f := ofHom₂ <| LinearMap.compr₂ (TensorProduct.mk R N M) ((β_ N M).hom ≫ f).hom
invFun f := (β_ M N).hom ≫ ofHom (TensorProduct.lift f.hom₂)
left_inv
f := by
ext : 1
apply TensorProduct.ext'
solve_by_elim
