mathlib3 documentation

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 #

Main results #

@[protected, instance]
def alternating_map.module_add_comm_group {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] {ι : Type u_4} :
module R (alternating_map R M N ι)
Equations
def exterior_algebra.lift_alternating {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module 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] [add_comm_group M] [add_comm_group N] [module R M] [module R N] (f : Π (i : ), alternating_map R M N (fin i)) (m : M) :
@[simp]
theorem exterior_algebra.lift_alternating_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] (f : Π (i : ), alternating_map R M N (fin i)) :
@[simp]
theorem exterior_algebra.lift_alternating_algebra_map {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] (f : Π (i : ), alternating_map R M N (fin i)) (r : R) :
@[simp]
theorem exterior_algebra.lift_alternating_apply_ι_multi {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] {n : } (f : Π (i : ), alternating_map R M N (fin i)) (v : fin n M) :
@[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 M] [add_comm_group N] [add_comm_group N'] [module R M] [module R N] [module R N'] (g : N →ₗ[R] N') (f : Π (i : ), alternating_map R M N (fin i)) :
@[ext]

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]