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 : ℕ) => ↥((TensorAlgebra.ι R).range ^ i)

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

Equations

• TensorAlgebra.GradedAlgebra.ι R M = DirectSum.lof R ℕ (fun (i : ℕ) => ↥((TensorAlgebra.ι R).range ^ i)) 1 ∘ₗ LinearMap.codRestrict ((TensorAlgebra.ι R).range ^ 1) (TensorAlgebra.ι R) ⋯

theorem TensorAlgebra.GradedAlgebra.ι_apply (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) : (ι R M) m = (DirectSum.of (fun (i : ℕ) => ↥((TensorAlgebra.ι R).range ^ 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 : ℕ) => (ι R).range ^ x

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

Equations

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