mathlib documentation

linear_algebra.exterior_algebra.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 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] [add_comm_group M] [module R M] :

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

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

Equations
@[protected, instance]

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

Equations