English
A more bundled version of domCoprodDep, viewed as a linear map from the tensor product of spaces of multilinear maps to the multilinear maps on the coproduct domain, i.e., domCoprodDep' := TensorProduct.lift (LinearMap.mk₂ R domCoprod (…)).
Русский
Более упорядоченная версия domCoprodDep — линейное отображение из тензорного произведения пространств мультиланейных отображений в мультиланейное отображение на копродомене: domCoprodDep' := TensorProduct.lift (LinearMap.mk₂ R domCoprod …).
LaTeX
$$$\text{There is a linear map } domCoprodDep' :\; (\mathrm{MultilinearMap}\,R\,(\lambda i_1. N(\mathrm{Sum}.inl\,i_1))\,N_1) \otimes_R (\mathrm{MultilinearMap}\,R\,(\lambda i_2. N(\mathrm{Sum}.inr\,i_2))\,N_2) \to_L_R \mathrm{MultilinearMap}\,R\,N\,(N_1\otimes_R N_2).$$$$
Lean4
/-- A more bundled version of `MultilinearMap.domCoprodDep`, as a linear map
from the tensor product of spaces of multilinear maps. -/
def domCoprodDep' :
MultilinearMap R (fun i₁ ↦ N (.inl i₁)) N₁ ⊗[R] MultilinearMap R (fun i₂ ↦ N (.inr i₂)) N₂ →ₗ[R]
MultilinearMap R N (N₁ ⊗[R] N₂) :=
TensorProduct.lift (LinearMap.mk₂ R domCoprodDep (by aesop) (by aesop) (by aesop) (by aesop))
