mathlib documentation


Results about the grading structure of the tensor algebra #

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

def tensor_algebra.graded_algebra.ι (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] :

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

@[protected, instance]

The tensor algebra is graded by the powers of the submodule (tensor_algebra.ι R).range.