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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_5} :

Module R (AlternatingMap R M N ι)

source

def ExteriorAlgebra.liftAlternating {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] :

((i : ℕ) → AlternatingMap R M N (Fin i)) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N

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

Instances For

source

@[simp]

theorem ExteriorAlgebra.liftAlternating_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : (i : ℕ) → AlternatingMap R M N (Fin i)) (m : M) :

↑(↑ExteriorAlgebra.liftAlternating f) (↑(ExteriorAlgebra.ι R) m) = ↑(f 1) ![m]

source

theorem ExteriorAlgebra.liftAlternating_ι_mul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : (i : ℕ) → AlternatingMap R M N (Fin i)) (m : M) (x : ExteriorAlgebra R M) :

↑(↑ExteriorAlgebra.liftAlternating f) (↑(ExteriorAlgebra.ι R) m * x) = ↑(↑ExteriorAlgebra.liftAlternating fun i => ↑(AlternatingMap.curryLeft (f (Nat.succ i))) m) x

source

@[simp]

theorem ExteriorAlgebra.liftAlternating_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : (i : ℕ) → AlternatingMap R M N (Fin i)) :

↑(↑ExteriorAlgebra.liftAlternating f) 1 = ↑(f 0) 0

source

@[simp]

theorem ExteriorAlgebra.liftAlternating_algebraMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : (i : ℕ) → AlternatingMap R M N (Fin i)) (r : R) :

↑(↑ExteriorAlgebra.liftAlternating f) (↑(algebraMap R (ExteriorAlgebra R M)) r) = r • ↑(f 0) 0

source

@[simp]

theorem ExteriorAlgebra.liftAlternating_apply_ιMulti {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : (i : ℕ) → AlternatingMap R M N (Fin i)) (v : Fin n → M) :

↑(↑ExteriorAlgebra.liftAlternating f) (↑(ExteriorAlgebra.ιMulti R n) v) = ↑(f n) v

source

@[simp]

theorem ExteriorAlgebra.liftAlternating_comp_ιMulti {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : (i : ℕ) → AlternatingMap R M N (Fin i)) :

↑(LinearMap.compAlternatingMap (↑ExteriorAlgebra.liftAlternating f)) (ExteriorAlgebra.ιMulti R n) = f n

source

@[simp]

theorem ExteriorAlgebra.liftAlternating_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup N'] [Module R M] [Module R N] [Module R N'] (g : N →ₗ[R] N') (f : (i : ℕ) → AlternatingMap R M N (Fin i)) :

(↑ExteriorAlgebra.liftAlternating fun i => ↑(LinearMap.compAlternatingMap g) (f i)) = LinearMap.comp g (↑ExteriorAlgebra.liftAlternating f)

source

@[simp]

theorem ExteriorAlgebra.liftAlternating_ιMulti {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :

↑ExteriorAlgebra.liftAlternating (ExteriorAlgebra.ιMulti R) = LinearMap.id

source

@[simp]

theorem ExteriorAlgebra.liftAlternatingEquiv_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (a : (i : ℕ) → AlternatingMap R M N (Fin i)) :

↑ExteriorAlgebra.liftAlternatingEquiv a = ↑ExteriorAlgebra.liftAlternating a

source

@[simp]

theorem ExteriorAlgebra.liftAlternatingEquiv_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (F : ExteriorAlgebra R M →ₗ[R] N) (i : ℕ) :

↑(LinearEquiv.symm ExteriorAlgebra.liftAlternatingEquiv) F i = ↑(LinearMap.compAlternatingMap F) (ExteriorAlgebra.ιMulti R i)

source

def ExteriorAlgebra.liftAlternatingEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] :

((i : ℕ) → AlternatingMap R M N (Fin i)) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N

ExteriorAlgebra.liftAlternating is an equivalence.

Instances For

source

theorem ExteriorAlgebra.lhom_ext {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] ⦃f : ExteriorAlgebra R M →ₗ[R] N⦄ ⦃g : ExteriorAlgebra R M →ₗ[R] N⦄ (h : ∀ (i : ℕ), ↑(LinearMap.compAlternatingMap f) (ExteriorAlgebra.ιMulti R i) = ↑(LinearMap.compAlternatingMap g) (ExteriorAlgebra.ι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]