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]
:
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, ⋯⟩
noncomputable 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)) ⋯ ⋯