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.

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) }

instance TensorAlgebra.gradedAlgebra {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : GradedAlgebra fun x => LinearMap.range (TensorAlgebra.ι R) ^ x

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