English
There is a linear equivalence between multilinear maps induced by a domain permutation σ: MultilinearMap R M1 M2 ≃ MultilinearMap R (fun i => M1 (σ.symm i)) M2.
Русский
Существует линейное эквивалентное отображение между мультиленейными отображениями, индуцируемое перестановкой домена: MultilinearMap R M1 M2 ≃ MultilinearMap R (fun i => M1 (σ.symm i)) M2.
LaTeX
$$$$ \text{domDomCongrLinearEquiv}(σ):\ MultilinearMap R M_1 M_2 \cong_\ell[S] MultilinearMap R (\lambda i. M_1(σ^{-1}(i))) M_2. $$$$
Lean4
/-- The space of constant maps is equivalent to the space of maps that are multilinear with respect
to an empty family. -/
@[simps]
def constLinearEquivOfIsEmpty [IsEmpty ι] : M₂ ≃ₗ[S] MultilinearMap R M₁ M₂
where
toFun := MultilinearMap.constOfIsEmpty R _
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun f := f 0
right_inv f := ext fun _ => MultilinearMap.congr_arg f <| Subsingleton.elim _ _
