English
In the monoidal category of modules over a commutative ring R, with unit object R and the usual tensor product, the triangle identity holds: the associator α_{M,R,N} composed with the left unitor λ_N is equal to the right unitor ρ_M tensored with the identity on N.
Русский
В моноидальной категории модулей над R справедливо треугольное тождество: ассоциатор α_{M,R,N} после левого унитора λ_N равен правому унитору ρ_M тензорно с идентичностью на N.
LaTeX
$$$ \alpha_{M, \mathbf{1}, N} \; \circ \; (\mathrm{id}_M \otimes \lambda_N) = (\rho_M \otimes \mathrm{id}_N).$$$
Lean4
theorem triangle (M N : ModuleCat.{u} R) :
(associator M (ModuleCat.of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom =
tensorHom (rightUnitor M).hom (𝟙 N) :=
by
ext : 1
apply TensorProduct.ext_threefold
intro x y
exact TensorProduct.tmul_smul _ _
