English
Given a family f_i of alternating maps f_i: M [⋀^Fin i] → N for each i, there exists a unique linear map ExteriorAlgebra R M → N extending all f_i on the corresponding exterior powers; i.e., liftAlternating(f) is the unique extension with lift on each i equal to f_i.
Русский
Существут единственное линейное отображение, которое расширяет все f_i на соответствующие внешние степени; liftAlternating обеспечивает универсальность расширения.
LaTeX
$$$liftAlternating: \prod_i (M [⋀^Fin i]→ₗ[R] N) \to (ExteriorAlgebra R M →ₗ[R] N)$ является универсальным продолжением, удовлетворяющим $liftAlternating(f) \circ ιMulti_R i = f_i$ для всех i$$
Lean4
/-- Build a map out of the exterior algebra given a collection of alternating maps acting on each
exterior power -/
def liftAlternating : (∀ i, M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N :=
by
suffices (∀ i, M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] ∀ i, M [⋀^Fin i]→ₗ[R] N
by
refine LinearMap.compr₂ this ?_
refine (LinearEquiv.toLinearMap ?_).comp (LinearMap.proj 0)
exact AlternatingMap.constLinearEquivOfIsEmpty.symm
refine CliffordAlgebra.foldl _ ?_ ?_
· refine
LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_) (fun m f₁ f₂ => ?_)
fun c m f => ?_
all_goals
ext i : 1
simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]
· -- when applied twice with the same `m`, this recursive step produces 0
intro m x
ext
simp
