Results about the grading structure of the tensor algebra #

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

def TensorAlgebra.GradedAlgebra.ι (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] :
M →ₗ[R] ⨁ (i : ), { x // x LinearMap.range (TensorAlgebra.ι R) ^ i }

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

Instances For
    theorem TensorAlgebra.GradedAlgebra.ι_apply (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) :
    ↑(TensorAlgebra.GradedAlgebra.ι R M) m = ↑(DirectSum.of (fun i => { x // x LinearMap.range (TensorAlgebra.ι R) ^ i }) 1) { val := ↑(TensorAlgebra.ι R) m, property := (_ : ↑(TensorAlgebra.ι R) m LinearMap.range (TensorAlgebra.ι R) ^ 1) }

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