monoidalClosed_curry — Mathlib

English

There is an equivalence between morphisms from the tensorLeft functor applied to N into P and morphisms from N to a linearCoyoneda object; concretely, Hom((M ⊗ N) ⟶ P) ≃ (N ⟶ Hom(M,P)).

Русский

Существует эквалентность между отображениями из (M ⊗ N) в P и отображениями из N в Hom(M,P).

LaTeX

$$$\\hom((M \\otimes N) \\to P) \\cong \\hom(N, \\operatorname{Hom}(M,P))$$$

Lean4

theorem monoidalClosed_curry {M N P : ModuleCat.{u} R} (f : M ⊗ N ⟶ P) (x : M) (y : N) :
    ((MonoidalClosed.curry f).hom y).hom x = f (x ⊗ₜ[R] y) :=
  rfl

Похожие утверждения