English
The standard triangle identity holds in ModuleCat with the associator and unitors; i.e., the two ways of rebracketing M ⊗ I ⊗ N are equal via associator and unitors.
Русский
В ModuleCat выполняется стандартное треугольное тождество для ассоциатора и единичных объектов; два способа переразбиения M ⊗ I ⊗ N совпадают.
LaTeX
$$$(\\alpha_{M,I,N})_{hom} \\circ (\\mathrm{tensorHom} (\\mathbb{1}_M) (\\mathrm{leftUnitor} N).hom) = (\\mathrm{rightUnitor} M).hom (\\mathbb{1}_N)$$$
Lean4
/-- Describes the counit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this
should give a map `M ⊗ Hom(M, N) ⟶ N`, so we flip the order of the arguments in the identity map
`Hom(M, N) ⟶ (M ⟶ N)` and uncurry the resulting map `M ⟶ Hom(M, N) ⟶ N.` -/
theorem ihom_ev_app (M N : ModuleCat.{u} R) :
(ihom.ev M).app N =
ModuleCat.ofHom
(TensorProduct.uncurry R M ((ihom M).obj N) N
(LinearMap.lcomp _ _ homLinearEquiv.toLinearMap ∘ₗ LinearMap.id.flip)) :=
by
rw [← MonoidalClosed.uncurry_id_eq_ev]
ext : 1
apply TensorProduct.ext'
apply monoidalClosed_uncurry
