English
If two linear maps from ExteriorAlgebra R M to N agree on all exterior powers via compAlternatingMap with ιMulti, then the maps are equal; this is a standard extensional principle for exterior algebras.
Русский
Если два линейных отображения от ExteriorAlgebra_R(M) к N совпадают на всех степенях через compAlternatingMap с ιMulti, они равны; это стандартная лемма экстензийной теории внешних степеней.
LaTeX
$$@[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$$
Lean4
/-- `exteriorAlgebra.ιMulti` is the alternating map from `Fin n → M` to `⋀[r]^n M`
induced by `exteriorAlgebra.ιMulti`, i.e. sending a family of vectors `m : Fin n → M` to the
product of its entries. -/
def ιMulti : M [⋀^Fin n]→ₗ[R] (⋀[R]^n M) :=
(ExteriorAlgebra.ιMulti R n).codRestrict (⋀[R]^n M) fun _ => ExteriorAlgebra.ιMulti_range R n <| Set.mem_range_self _
