English
The map liftAlternatingEquiv provides a linear equivalence between the family of alternating maps and linear maps from ExteriorAlgebra to N; it has explicit left and right inverses described by projectors onto exterior powers.
Русский
Лифтинг-эквивалент дает линейное эквивалентство между семейством чередующихся отображений и линейными отображениями из ExteriorAlgebra в N; существуют явные левые и правые обратные стороны через проекции на внешние степени.
LaTeX
$$$liftAlternatingEquiv: (\forall i, M [⋀^Fin i]→ₗ[R] N) \cong_L[R] ExteriorAlgebra R M →ₗ[R] N$$$
Lean4
/-- To show that two linear maps from the exterior algebra agree, it suffices to show they agree on
the exterior powers.
See note [partially-applied ext lemmas] -/
@[ext]
theorem lhom_ext ⦃f g : ExteriorAlgebra R M →ₗ[R] N⦄
(h : ∀ i, f.compAlternatingMap (ιMulti R i) = g.compAlternatingMap (ιMulti R i)) : f = g :=
liftAlternatingEquiv.symm.injective <| funext h
