English
Two linear maps from ExteriorAlgebra R M to N are equal if they agree on all ExteriorPower components; this extensional principle follows from liftAlternatingEquiv being an equivalence.
Русский
Два линейных отображения из ExteriorAlgebra_R(M) в N равны, если они совпадают на всех компонентах ExteriorPower; следует из того, что liftAlternatingEquiv – эквалентность.
LaTeX
$$@@@ extensional principle: if ∀ i, f ∘AlternatingMap(ιMulti i) = g ∘AlternatingMap(ιMulti i) then f=g$$
Lean4
@[simp]
theorem liftAlternating_comp (g : N →ₗ[R] N') (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) :
(liftAlternating (R := R) (M := M) (N := N') fun i => g.compAlternatingMap (f i)) =
g ∘ₗ liftAlternating (R := R) (M := M) (N := N) f :=
by
ext v
rw [LinearMap.comp_apply]
induction v using CliffordAlgebra.left_induction generalizing f with
| algebraMap =>
rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul, LinearMap.compAlternatingMap_apply]
| add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
| ι_mul _ _ hx =>
rw [liftAlternating_ι_mul, liftAlternating_ι_mul, ← hx]
simp_rw [AlternatingMap.curryLeft_compAlternatingMap]
