# Extending an alternating map to the exterior algebra #

## Main definitions #

• ExteriorAlgebra.liftAlternating: construct a linear map out of the exterior algebra given alternating maps (corresponding to maps out of the exterior powers).
• ExteriorAlgebra.liftAlternatingEquiv: the above as a linear equivalence

## Main results #

• ExteriorAlgebra.lhom_ext: linear maps from the exterior algebra agree if they agree on the exterior powers.
instance AlternatingMap.instModuleAddCommGroup {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] {ι : Type u_5} :
Equations
def ExteriorAlgebra.liftAlternating {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] :
((i : ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] →ₗ[R] N

Build a map out of the exterior algebra given a collection of alternating maps acting on each exterior power

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ExteriorAlgebra.liftAlternating_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (f : (i : ) → M [⋀^Fin i]→ₗ[R] N) (m : M) :
(ExteriorAlgebra.liftAlternating f) ( m) = (f 1) ![m]
theorem ExteriorAlgebra.liftAlternating_ι_mul {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (f : (i : ) → M [⋀^Fin i]→ₗ[R] N) (m : M) (x : ) :
(ExteriorAlgebra.liftAlternating f) ( m * x) = (ExteriorAlgebra.liftAlternating fun (i : ) => (f i.succ).curryLeft m) x
@[simp]
theorem ExteriorAlgebra.liftAlternating_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (f : (i : ) → M [⋀^Fin i]→ₗ[R] N) :
(ExteriorAlgebra.liftAlternating f) 1 = (f 0) 0
@[simp]
theorem ExteriorAlgebra.liftAlternating_algebraMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (f : (i : ) → M [⋀^Fin i]→ₗ[R] N) (r : R) :
(ExteriorAlgebra.liftAlternating f) ((algebraMap R ()) r) = r (f 0) 0
@[simp]
theorem ExteriorAlgebra.liftAlternating_apply_ιMulti {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] {n : } (f : (i : ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin nM) :
(ExteriorAlgebra.liftAlternating f) (() v) = (f n) v
@[simp]
theorem ExteriorAlgebra.liftAlternating_comp_ιMulti {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] {n : } (f : (i : ) → M [⋀^Fin i]→ₗ[R] N) :
(ExteriorAlgebra.liftAlternating f).compAlternatingMap () = f n
@[simp]
theorem ExteriorAlgebra.liftAlternating_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [] [] [] [] [Module R M] [Module R N] [Module R N'] (g : N →ₗ[R] N') (f : (i : ) → M [⋀^Fin i]→ₗ[R] N) :
(ExteriorAlgebra.liftAlternating fun (i : ) => g.compAlternatingMap (f i)) = g ∘ₗ ExteriorAlgebra.liftAlternating f
@[simp]
theorem ExteriorAlgebra.liftAlternating_ιMulti {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
ExteriorAlgebra.liftAlternating = LinearMap.id
@[simp]
theorem ExteriorAlgebra.liftAlternatingEquiv_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (a : (i : ) → M [⋀^Fin i]→ₗ[R] N) :
ExteriorAlgebra.liftAlternatingEquiv a = ExteriorAlgebra.liftAlternating a
@[simp]
theorem ExteriorAlgebra.liftAlternatingEquiv_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] (F : →ₗ[R] N) (i : ) :
ExteriorAlgebra.liftAlternatingEquiv.symm F i = F.compAlternatingMap ()
def ExteriorAlgebra.liftAlternatingEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] :
((i : ) → M [⋀^Fin i]→ₗ[R] N) ≃ₗ[R] →ₗ[R] N

ExteriorAlgebra.liftAlternating is an equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ExteriorAlgebra.lhom_ext {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] ⦃f : →ₗ[R] N ⦃g : →ₗ[R] N (h : ∀ (i : ), f.compAlternatingMap () = g.compAlternatingMap ()) :
f = g

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]