Documentation

Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Extending an alternating map to the exterior algebra #

Main definitions #

Main results #

source
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 (M [Λ^ι]→ₗ[R] N)
Equations
  • AlternatingMap.instModuleAddCommGroup = inferInstance
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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) →ₗ[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

Equations
  • One or more equations did not get rendered due to their size.
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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) (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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) (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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) :
    (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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) (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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) (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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) :
    (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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) :
    (ExteriorAlgebra.liftAlternating fun (i : ℕ) => (LinearMap.compAlternatingMap g) (f i)) = 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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) :
    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 : ℕ) → M [Λ^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N

    ExteriorAlgebra.liftAlternating is an equivalence.

    Equations
    • One or more equations did not get rendered due to their size.
    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]