English
The domain-dom congruence functor is invertible, giving an equivalence of maps under permutation.
Русский
Функтор доменного преобразования является эквивалентностью, сохраняющей карты под перестановками.
LaTeX
$$def domDomCongrEquiv (σ) : MultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃+ MultilinearMap R (fun _ : ι₂ => M₂) M₃$$
Lean4
/-- `MultilinearMap.domDomCongr` as an equivalence.
This is declared separately because it does not work with dot notation. -/
@[simps apply symm_apply]
def domDomCongrEquiv (σ : ι₁ ≃ ι₂) : MultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃+ MultilinearMap R (fun _ : ι₂ => M₂) M₃
where
toFun := domDomCongr σ
invFun := domDomCongr σ.symm
left_inv
m := by
ext
simp [domDomCongr]
right_inv
m := by
ext
simp [domDomCongr]
map_add' a
b := by
ext
simp [domDomCongr]
