Documentation

Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Extending an alternating map to the exterior algebra #

Main definitions #

Main results #

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} :
Equations
  • AlternatingMap.instModuleAddCommGroup = inferInstance
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_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 : ) → M [⋀^Fin i]→ₗ[R] N) :
    (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 : ) → 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 nM) :
    (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) :
    (ExteriorAlgebra.liftAlternating fun (i : ) => g.compAlternatingMap (f i)) = 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_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)
    @[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 : ) → M [⋀^Fin i]→ₗ[R] N) :
    ExteriorAlgebra.liftAlternatingEquiv a = ExteriorAlgebra.liftAlternating a
    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]