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 ι)
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
@[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]
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
@[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
@[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
@[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
@[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
@[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)
@[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
@[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
@[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)
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
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]