English
There is a linear equivalence between n-fold alternating maps M → N and linear maps from the exterior power ⋀[R]^n M to N.
Русский
Существует линейное эквивалентное отображение между чередующимися отображениями в n аргументов M → N и линейными отображениями от ⋀^n_R M к N.
LaTeX
$$$\\text{alternatingMapLinearEquiv} : (M [⋀^Fin n]→_R N) \\simeq_R (⋀[R]^n M) →_R N$$$
Lean4
/-- The linear equivalence between `n`-fold alternating maps from `M` to `N` and linear maps from
`⋀[R]^n M` to `N`: this is the universal property of the `n`th exterior power of `M`. -/
noncomputable def alternatingMapLinearEquiv : (M [⋀^Fin n]→ₗ[R] N) ≃ₗ[R] ⋀[R]^n M →ₗ[R] N :=
LinearEquiv.symm
(Equiv.toLinearEquiv ((presentation R n M).linearMapEquiv.trans presentation.relationsSolutionEquiv)
{ map_add := fun _ _ => rfl
map_smul := fun _ _ => rfl })
