# mathlibdocumentation

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

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

def exterior_algebra.graded_algebra.ι (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] :
M →ₗ[R] (λ (i : ), .range ^ i))

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

Equations
theorem exterior_algebra.graded_algebra.ι_apply (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] (m : M) :
= (direct_sum.of (λ (i : ), .range ^ i)) 1) m, _⟩
theorem exterior_algebra.graded_algebra.ι_sq_zero (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] (m : M) :
= 0
def exterior_algebra.graded_algebra.lift_ι (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] :
→ₐ[R] (λ (i : ), .range ^ i))

exterior_algebra.graded_algebra.ι lifted to exterior algebra. This is primarily an auxiliary construction used to provide exterior_algebra.graded_algebra.

Equations
• = _inst_3, _⟩
theorem exterior_algebra.graded_algebra.lift_ι_eq {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (i : ) (x : .range ^ i)) :
= (direct_sum.of (λ (i : ), .range ^ i)) i) x
@[protected, instance]
def exterior_algebra.graded_algebra {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] :

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

Equations