map_apply_ιMulti — Mathlib

English

There is a linear equivalence between alternating maps M → N and linear maps from wedge^n_R M to N, realized by alternatingMapLinearEquiv.

Русский

Существует линейное эквивалентное отображение между чередующимися отображениями M → N и линейными отображениями из ⋀^n_R M в N посредством alternatingMapLinearEquiv.

LaTeX

$$$\\text{alternatingMapLinearEquiv} : (M [⋀^Fin n]→_R N) ≃_l_R (⋀[R]^n M →_l_R N)$$$

Lean4

@[simp]
theorem map_apply_ιMulti (f : M →ₗ[R] N) (m : Fin n → M) : map n f (ιMulti R n m) = ιMulti R n (f ∘ m) := by
  simp only [map, alternatingMapLinearEquiv_apply_ιMulti, AlternatingMap.compLinearMap_apply, Function.comp_def]

Похожие утверждения