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.

def ExteriorAlgebra.GradedAlgebra.ι (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :
M →ₗ[R] ⨁ (i : ), { x // x 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.

Instances For
    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 => { x // x LinearMap.range (ExteriorAlgebra.ι R) ^ i }) 1) { val := ↑(ExteriorAlgebra.ι R) m, property := (_ : ↑(ExteriorAlgebra.ι R) m LinearMap.range (ExteriorAlgebra.ι R) ^ 1) }

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

    Instances For
      theorem ExteriorAlgebra.GradedAlgebra.liftι_eq (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (i : ) (x : { x // x LinearMap.range (ExteriorAlgebra.ι R) ^ i }) :

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