Documentation

Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Results about the grading structure of the exterior algebra #

Many of these results are copied with minimal modification from the tensor algebra.

The main result is ExteriorAlgebra.gradedAlgebra, which says that the exterior algebra is a ℕ-graded algebra.

source
def ExteriorAlgebra.GradedAlgebra.ι (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :
M →ₗ[R] DirectSum ℕ fun (i : ℕ) => ↥(LinearMap.range (ExteriorAlgebra.ι R) ^ i)

A version of ExteriorAlgebra.ι that maps directly into the graded structure. This is primarily an auxiliary construction used to provide ExteriorAlgebra.gradedAlgebra.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ExteriorAlgebra.GradedAlgebra.ι_apply (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (m : M) :
    (ExteriorAlgebra.GradedAlgebra.ι R M) m = (DirectSum.of (fun (i : ℕ) => ↥(LinearMap.range (ExteriorAlgebra.ι R) ^ i)) 1) { val := (ExteriorAlgebra.ι R) m, property := (_ : (ExteriorAlgebra.ι R) m ∈ LinearMap.range (ExteriorAlgebra.ι R) ^ 1) }
    source
    theorem ExteriorAlgebra.GradedAlgebra.ι_sq_zero (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (m : M) :
    (ExteriorAlgebra.GradedAlgebra.ι R M) m * (ExteriorAlgebra.GradedAlgebra.ι R M) m = 0
    source
    def ExteriorAlgebra.GradedAlgebra.liftι (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :
    ExteriorAlgebra R M →ₐ[R] DirectSum ℕ fun (i : ℕ) => ↥(LinearMap.range (ExteriorAlgebra.ι R) ^ i)

    ExteriorAlgebra.GradedAlgebra.ι lifted to exterior algebra. This is primarily an auxiliary construction used to provide ExteriorAlgebra.gradedAlgebra.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem ExteriorAlgebra.GradedAlgebra.liftι_eq (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (x : ↥(LinearMap.range (ExteriorAlgebra.ι R) ^ i)) :
      (ExteriorAlgebra.GradedAlgebra.liftι R M) ↑x = (DirectSum.of (fun (i : ℕ) => ↥(LinearMap.range (ExteriorAlgebra.ι R) ^ i)) i) x
      source
      instance ExteriorAlgebra.gradedAlgebra (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :
      GradedAlgebra fun (x : ℕ) => LinearMap.range (ExteriorAlgebra.ι R) ^ x

      The exterior algebra is graded by the powers of the submodule (ExteriorAlgebra.ι R).range.

      Equations
      • One or more equations did not get rendered due to their size.