# mathlib3documentation

linear_algebra.exterior_algebra.of_alternating

# Extending an alternating map to the exterior algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• exterior_algebra.lift_alternating: construct a linear map out of the exterior algebra given alternating maps (corresponding to maps out of the exterior powers).
• exterior_algebra.lift_alternating_equiv: the above as a linear equivalence

## Main results #

• exterior_algebra.lhom_ext: linear maps from the exterior algebra agree if they agree on the exterior powers.
@[protected, instance]
def alternating_map.module_add_comm_group {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] {ι : Type u_4} :
M N ι)
Equations
def exterior_algebra.lift_alternating {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] :
(Π (i : ), N (fin i)) →ₗ[R] →ₗ[R] N

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

Equations
@[simp]
theorem exterior_algebra.lift_alternating_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] (f : Π (i : ), N (fin i)) (m : M) :
= (f 1) ![m]
theorem exterior_algebra.lift_alternating_ι_mul {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] (f : Π (i : ), N (fin i)) (m : M) (x : M) :
@[simp]
theorem exterior_algebra.lift_alternating_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] (f : Π (i : ), N (fin i)) :
= (f 0) 0
@[simp]
theorem exterior_algebra.lift_alternating_algebra_map {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] (f : Π (i : ), N (fin i)) (r : R) :
( M)) r) = r (f 0) 0
@[simp]
theorem exterior_algebra.lift_alternating_apply_ι_multi {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] {n : } (f : Π (i : ), N (fin i)) (v : fin n M) :
= (f n) v
@[simp]
theorem exterior_algebra.lift_alternating_comp_ι_multi {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] {n : } (f : Π (i : ), N (fin i)) :
@[simp]
theorem exterior_algebra.lift_alternating_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [comm_ring R] [add_comm_group N'] [ M] [ N] [ N'] (g : N →ₗ[R] N') (f : Π (i : ), N (fin i)) :
@[simp]
theorem exterior_algebra.lift_alternating_ι_multi {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] :
@[simp]
theorem exterior_algebra.lift_alternating_equiv_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] (ᾰ : Π (i : ), N (fin i)) :
def exterior_algebra.lift_alternating_equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] :
(Π (i : ), N (fin i)) ≃ₗ[R] →ₗ[R] N

exterior_algebra.lift_alternating is an equivalence.

Equations
@[simp]
theorem exterior_algebra.lift_alternating_equiv_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] (F : →ₗ[R] N) (i : ) :
@[ext]
theorem exterior_algebra.lhom_ext {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [ M] [ N] ⦃f g : →ₗ[R] N⦄ (h : (i : ), ) :
f = g

To show that two linear maps from the exterior algebra agree, it suffices to show they agree on the exterior powers.