English
The alternating map linear equivalence respects composition with a linear map; composing f with a linear map agrees with composing the corresponding wedge map with the same linear map.
Русский
Чередующeеся линейное эквивалентности сохраняют композицию с линейным отображением: композиция f с линейным отображением соответствует композиции соответствующего клина-отображения с тем же линейным отображением.
LaTeX
$$$\\text{alternatingMapLinearEquiv}(g\\circ f) = g\\circ (\\text{alternatingMapLinearEquiv}(f))$$$
Lean4
/-- If `f` is an alternating map from `M` to `N`,
`alternatingMapLinearEquiv f` is the corresponding linear map from `⋀[R]^n M` to `N`,
and if `g` is a linear map from `N` to `N'`, then
the alternating map `g.compAlternatingMap f` from `M` to `N'` corresponds to the linear
map `g.comp (alternatingMapLinearEquiv f)` on `⋀[R]^n M`. -/
theorem alternatingMapLinearEquiv_comp (g : N →ₗ[R] N') (f : M [⋀^Fin n]→ₗ[R] N) :
alternatingMapLinearEquiv (g.compAlternatingMap f) = g.comp (alternatingMapLinearEquiv f) :=
by
ext
simp only [alternatingMapLinearEquiv_comp_ιMulti, LinearMap.compAlternatingMap_apply, LinearMap.coe_comp, comp_apply,
alternatingMapLinearEquiv_apply_ιMulti]
