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.
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]
:
Build a map out of the exterior algebra given a collection of alternating maps acting on each exterior power
Equations
- One or more equations did not get rendered due to their size.
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 : ℕ) → M [⋀^Fin i]→ₗ[R] N)
(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 : ℕ) → M [⋀^Fin i]→ₗ[R] N)
(m : M)
(x : ExteriorAlgebra R M)
:
(ExteriorAlgebra.liftAlternating f) ((ExteriorAlgebra.ι R) m * x) = (ExteriorAlgebra.liftAlternating fun (i : ℕ) => (f i.succ).curryLeft m) x
@[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 : ℕ) → M [⋀^Fin i]→ₗ[R] N)
(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 : ℕ) → M [⋀^Fin i]→ₗ[R] N)
(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 : ℕ) → M [⋀^Fin i]→ₗ[R] N)
:
(ExteriorAlgebra.liftAlternating f).compAlternatingMap (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 : ℕ) → M [⋀^Fin i]→ₗ[R] N)
:
@[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_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 : ℕ)
:
ExteriorAlgebra.liftAlternatingEquiv.symm F i = F.compAlternatingMap (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]
:
ExteriorAlgebra.liftAlternating
is an equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ExteriorAlgebra.lhom_ext_iff
{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}
:
f = g ↔ ∀ (i : ℕ), f.compAlternatingMap (ExteriorAlgebra.ιMulti R i) = g.compAlternatingMap (ExteriorAlgebra.ιMulti R i)
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 : ℕ), f.compAlternatingMap (ExteriorAlgebra.ιMulti R i) = g.compAlternatingMap (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]