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.
noncomputable def
TensorAlgebra.GradedAlgebra.ι
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
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)
:
noncomputable instance
TensorAlgebra.gradedAlgebra
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
The tensor algebra is graded by the powers of the submodule (TensorAlgebra.ι R).range
.