Documentation

Mathlib.LinearAlgebra.TensorAlgebra.Grading

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.

    Equations