mathlib documentation

linear_algebra.tensor_algebra.grading

Results about the grading structure of the tensor algebra #

The main result is tensor_algebra.graded_algebra, which says that the tensor algebra is a ℕ-graded algebra.

source
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
source
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, _⟩
source
@[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] :
graded_algebra (has_pow.pow (linear_map.range (tensor_algebra.ι R)))

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

Equations