English
Let R be a commutative semiring and M, N, P be R-modules. There is a natural linear isomorphism between linear maps from the tensor product M ⊗_R N to P and bilinear maps M × N → P. Concretely, the curry operation sends a linear map f: M ⊗_R N → P to the bilinear map M × N → P given by (m, n) ↦ f(m ⊗ n).
Русский
Пусть R – коммутативное полукольцо, M, N, P – модулы над R. Существуют естественные линейные изоморфизмы между линейными отображениями M ⊗_R N → P и билинейными отображениями M × N → P. Явление curry присваивает отображению f: M ⊗_R N → P билинейное отображение M × N → P, задаваемое (m, n) ↦ f(m ⊗ n).
LaTeX
$$$\\operatorname{lcurry} : \\operatorname{Hom}_R(M \\otimes_R N, P) \\to \\operatorname{Hom}_R(M, \\operatorname{Hom}_R(N, P))$, \\quad (\\mathrm{lcurry}(f))(m)(n) = f(m \\otimes n).$$
Lean4
/-- Given a linear map `M ⊗ N → P`, compose it with the canonical bilinear map `M → N → M ⊗ N` to
form a bilinear map `M → N → P`. -/
def lcurry : (M ⊗[R] N →ₗ[R] P) →ₗ[R] M →ₗ[R] N →ₗ[R] P :=
(lift.equiv R M N P).symm
