English
There is a canonical linear map from the n-th exterior power to the n-th tensor power of an R-module M, obtained by antisymmetrization of the universal multilinear map.
Русский
Существует каноническое линейное отображение из n-й внешней степени в n-й тензорной степени модуля M над R, получаемое антис симетризацией универсального мультилинейного отображения.
LaTeX
$$$ toTensorPower(R\, M\, n) : \ ⋀[R]^n M \rightarrowₗ[R] ⨂[R]^n M = \ operatorname{alternatingMapLinearEquiv}(\operatorname{MultilinearMap.alternatization}(\ PiTensorProduct.tprod R))$$$
Lean4
/-- The linear map from the `n`th exterior power to the `n`th tensor power obtained by
`MultilinearMap.alternatization`. -/
noncomputable def toTensorPower (n : ℕ) : ⋀[R]^n M →ₗ[R] ⨂[R]^n M :=
alternatingMapLinearEquiv (MultilinearMap.alternatization (PiTensorProduct.tprod R))
