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