English
The counit of the closed structure M ⊗ - ⊣ Hom(M,-) is realized by evaluation; at N the app is given by curry/uncurry correspondence between Hom(M,N) and M ⟶ N.
Русский
Падение counit для замкнутой структуры M ⊗ - ⊣ Hom(M,-) реализуется через вычисление; на объекте N отображение определяется через карри/анкюри соответствие между Hom(M,N) и M ⟶ N.
LaTeX
$$$(\\mathrm{ihom.ev}\\ M).\\mathrm{app}\\ N = \\mathrm{ModuleCat.ofHom}(\\mathrm{TensorProduct.uncurry}\\ R\\ M\\ ((\\mathrm{ihom } M).obj N) N (\\mathrm{LinearMap.lcomp}\\ _ _ \\mathrm{homLinearEquiv.toLinearMap} \\circ_!\\mathrm LinearMap.id.flip))$$$
Lean4
theorem id_tensorHom_id (M N : ModuleCat R) : tensorHom (𝟙 M) (𝟙 N) = 𝟙 (ModuleCat.of R (M ⊗ N)) :=
by
ext : 1
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): even with high priority `ext` fails to find this.
apply TensorProduct.ext
rfl
