# 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] DirectSum ℕ fun (i : ℕ) => ↥(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`

.

## Equations

- One or more equations did not get rendered due to their size.

## 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 : ℕ) => ↥(LinearMap.range (TensorAlgebra.ι R) ^ i)) 1) ⟨(TensorAlgebra.ι R) m, ⋯⟩

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`

.

## Equations

- TensorAlgebra.gradedAlgebra = GradedAlgebra.ofAlgHom (fun (x : ℕ) => LinearMap.range (TensorAlgebra.ι R) ^ x) ((TensorAlgebra.lift R) (TensorAlgebra.GradedAlgebra.ι R M)) ⋯ ⋯