mathlib documentation

linear_algebra.exterior_algebra.of_alternating

Extending an alternating map to the exterior algebra #

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} [decidable_eq ι] :
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) :
theorem exterior_algebra.lift_alternating_ι_mul {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) (x : exterior_algebra R 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_ι_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)) :
@[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)) :
@[simp]
@[ext]
theorem exterior_algebra.lhom_ext {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 g : exterior_algebra R M →ₗ[R] N⦄ (h : ∀ (i : ), (f.comp_alternating_map) (exterior_algebra.ι_multi R i) = (g.comp_alternating_map) (exterior_algebra.ι_multi R i)) :
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]