# 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) [] [] [Module R M] :
M →ₗ[R] DirectSum fun (i : ) => (⋀[R]^i M)

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

Equations
Instances For
theorem ExteriorAlgebra.GradedAlgebra.ι_apply (R : Type u_1) (M : Type u_2) [] [] [Module R M] (m : M) :
= (DirectSum.of (fun (i : ) => (⋀[R]^i M)) 1) m,
Equations
• =
theorem ExteriorAlgebra.GradedAlgebra.ι_sq_zero (R : Type u_1) (M : Type u_2) [] [] [Module R M] (m : M) :
* = 0
def ExteriorAlgebra.GradedAlgebra.liftι (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
→ₐ[R] DirectSum fun (i : ) => (⋀[R]^i M)

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

Equations
Instances For
theorem ExteriorAlgebra.GradedAlgebra.liftι_eq (R : Type u_1) (M : Type u_2) [] [] [Module R M] (i : ) (x : (⋀[R]^i M)) :
= (DirectSum.of (fun (i : ) => (⋀[R]^i M)) i) x
instance ExteriorAlgebra.gradedAlgebra (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
GradedAlgebra fun (i : ) => ⋀[R]^i M

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

Equations
theorem ExteriorAlgebra.ιMulti_span (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
Submodule.span R (Set.range fun (x : (n : ) × (Fin nM)) => (ExteriorAlgebra.ιMulti R x.fst) x.snd) =

The union of the images of the maps ExteriorAlgebra.ιMulti R n for n running through all natural numbers spans the exterior algebra.