English
The evaluation map ihom.ev M applied to N gives a canonical map that corresponds to composing with the evaluation; more precisely, (ihom.ev M).app N equals ofHom of a certain uncurry construction.
Русский
Оценочный отображение ihom.ev M, применённое к N, задаёт каноническое отображение, соответствующее композиции; точнее, (ihom.ev M).app N = ofHom(uncurry-конструкция).
LaTeX
$$$(\\mathrm{ihom.ev}\\ M).\\mathrm{app}\\ N = \\mathrm{ofHom}\\big(\\mathrm{TensorProduct.uncurry}\\;R\\;M\\;((\\mathrm{ihom}\\ M).obj N)\\;N\\;\\big)$$$
Lean4
/-- Describes the unit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this should
define a map `N ⟶ Hom(M, M ⊗ N)`, which is given by flipping the arguments in the natural
`R`-bilinear map `M ⟶ N ⟶ M ⊗ N`. -/
theorem ihom_coev_app (M N : ModuleCat.{u} R) : (ihom.coev M).app N = ModuleCat.ofHom₂ (TensorProduct.mk _ _ _).flip :=
rfl
