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
    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
      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) :
        (liftAlternating f) ((ι 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) :
        (liftAlternating f) ((ι R) m * x) = (liftAlternating fun (i : ℕ) => (f i.succ).curryLeft 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) :
        (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) :
        (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) :
        (liftAlternating f) ((ι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) :
        (liftAlternating f).compAlternatingMap (ι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) :
        (liftAlternating fun (i : ℕ) => g.compAlternatingMap (f i)) = g ∘ₗ liftAlternating f
        source
        @[simp]
        theorem ExteriorAlgebra.liftAlternating_ιMulti {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :
        liftAlternating (ιMulti R) = LinearMap.id
        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
          Instances For
            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) :
            liftAlternatingEquiv a = 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 : ℕ) :
            liftAlternatingEquiv.symm F i = F.compAlternatingMap (ιMulti R i)
            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 g : ExteriorAlgebra R M →ₗ[R] N⦄ (h : ∀ (i : ℕ), f.compAlternatingMap (ιMulti R i) = g.compAlternatingMap (ι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]

            source
            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 g : ExteriorAlgebra R M →ₗ[R] N} :
            f = g ↔ ∀ (i : ℕ), f.compAlternatingMap (ιMulti R i) = g.compAlternatingMap (ιMulti R i)