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]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
{ι : Type u_4} :
module R (alternating_map R M N ι)
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] :
(Π (i : ℕ), alternating_map R M N (fin i)) →ₗ[R] exterior_algebra R M →ₗ[R] N
Build a map out of the exterior algebra given a collection of alternating maps acting on each exterior power
Equations
- exterior_algebra.lift_alternating = (clifford_algebra.foldl 0 (linear_map.mk₂ R (λ (m : M) (f : Π (i : ℕ), alternating_map R M N (fin i)) (i : ℕ), ⇑((f i.succ).curry_left) m) exterior_algebra.lift_alternating._proof_3 exterior_algebra.lift_alternating._proof_4 exterior_algebra.lift_alternating._proof_5 exterior_algebra.lift_alternating._proof_6) exterior_algebra.lift_alternating._proof_7).compr₂ (alternating_map.const_linear_equiv_of_is_empty.symm.to_linear_map.comp (linear_map.proj 0))
@[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) :
⇑(⇑exterior_algebra.lift_alternating f) (⇑(exterior_algebra.ι R) 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]
[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) :
⇑(⇑exterior_algebra.lift_alternating f) (⇑(exterior_algebra.ι R) m * x) = ⇑(⇑exterior_algebra.lift_alternating (λ (i : ℕ), ⇑((f i.succ).curry_left) m)) x
@[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)) :
⇑(⇑exterior_algebra.lift_alternating f) 1 = ⇑(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]
[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) :
⇑(⇑exterior_algebra.lift_alternating f) (⇑(algebra_map R (exterior_algebra 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]
[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) :
⇑(⇑exterior_algebra.lift_alternating f) (⇑(exterior_algebra.ι_multi R n) v) = ⇑(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]
[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)) :
⇑exterior_algebra.lift_alternating (λ (i : ℕ), ⇑(g.comp_alternating_map) (f i)) = g.comp (⇑exterior_algebra.lift_alternating f)
@[simp]
theorem
exterior_algebra.lift_alternating_ι_multi
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module 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]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(ᾰ : Π (i : ℕ), alternating_map R M N (fin i)) :
def
exterior_algebra.lift_alternating_equiv
{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] :
(Π (i : ℕ), alternating_map R M N (fin i)) ≃ₗ[R] exterior_algebra R M →ₗ[R] N
exterior_algebra.lift_alternating is an equivalence.
Equations
- exterior_algebra.lift_alternating_equiv = {to_fun := ⇑exterior_algebra.lift_alternating, map_add' := _, map_smul' := _, inv_fun := λ (F : exterior_algebra R M →ₗ[R] N) (i : ℕ), ⇑(F.comp_alternating_map) (exterior_algebra.ι_multi R i), left_inv := _, right_inv := _}
@[simp]
theorem
exterior_algebra.lift_alternating_equiv_symm_apply
{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 : exterior_algebra R M →ₗ[R] N)
(i : ℕ) :
@[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.