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] 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

• ExteriorAlgebra.GradedAlgebra.ι R M = DirectSum.lof R ℕ (fun (i : ℕ) => ↥(⋀[R]^i M)) 1 ∘ₗ LinearMap.codRestrict (⋀[R]^1 M) (ExteriorAlgebra.ι R) ⋯

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 : ℕ) => ↥(⋀[R]^i M)) 1) ⟨(ExteriorAlgebra.ι R) m, ⋯⟩

instance ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : SetLike.GradedMonoid fun (i : ℕ) => ⋀[R]^i M

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

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 : ℕ) => ↥(⋀[R]^i M)

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

Equations

• ExteriorAlgebra.GradedAlgebra.liftι R M = (ExteriorAlgebra.lift R) ⟨ExteriorAlgebra.GradedAlgebra.ι R M, ⋯⟩

theorem ExteriorAlgebra.GradedAlgebra.liftι_eq (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (x : ↥(⋀[R]^i M)) : (ExteriorAlgebra.GradedAlgebra.liftι R M) ↑x = (DirectSum.of (fun (i : ℕ) => ↥(⋀[R]^i M)) i) x

instance ExteriorAlgebra.gradedAlgebra (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : GradedAlgebra fun (i : ℕ) => ⋀[R]^i M

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

Equations

• ExteriorAlgebra.gradedAlgebra R M = GradedAlgebra.ofAlgHom (fun (i : ℕ) => ⋀[R]^i M) (ExteriorAlgebra.GradedAlgebra.liftι R M) ⋯ ⋯

theorem ExteriorAlgebra.ιMulti_span (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : Submodule.span R (Set.range fun (x : (n : ℕ) × (Fin n → M)) => (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.