Results about the grading structure of the tensor algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The main result is tensor_algebra.graded_algebra, which says that the tensor algebra is a
ℕ-graded algebra.
def
tensor_algebra.graded_algebra.ι
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
M →ₗ[R] direct_sum ℕ (λ (i : ℕ), ↥(linear_map.range (tensor_algebra.ι R) ^ i))
A version of tensor_algebra.ι that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide tensor_algebra.graded_algebra.
Equations
- tensor_algebra.graded_algebra.ι R M = (direct_sum.lof R ℕ (λ (i : ℕ), ↥(linear_map.range (tensor_algebra.ι R) ^ i)) 1).comp (linear_map.cod_restrict (linear_map.range (tensor_algebra.ι R) ^ 1) (tensor_algebra.ι R) _)
theorem
tensor_algebra.graded_algebra.ι_apply
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(m : M) :
⇑(tensor_algebra.graded_algebra.ι R M) m = ⇑(direct_sum.of (λ (i : ℕ), ↥(linear_map.range (tensor_algebra.ι R) ^ i)) 1) ⟨⇑(tensor_algebra.ι R) m, _⟩
@[protected, instance]
def
tensor_algebra.graded_algebra
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
The tensor algebra is graded by the powers of the submodule (tensor_algebra.ι R).range.
Equations
- tensor_algebra.graded_algebra = graded_algebra.of_alg_hom (has_pow.pow (linear_map.range (tensor_algebra.ι R))) (⇑(tensor_algebra.lift R) (tensor_algebra.graded_algebra.ι R M)) tensor_algebra.graded_algebra._proof_7 tensor_algebra.graded_algebra._proof_8