Tensor product of graded vector spaces

Let $𝑉, 𝑊$ be $𝔄$ -graded vector spaces over $𝕂$ for some monoid $(𝔄, +)$ . The tensor product $𝑉 \otimes 𝑊$ is the $𝕂$ -tensor product of vector spaces with the unique $𝔄$ -gradation specified by #m/def/linalg

𝑉 𝛼 \otimes 𝑊 𝛽 \leq (𝑉 \otimes 𝑊) 𝛼 + 𝛽

for all $𝛼, 𝛽 \in 𝔄$ . This extends to any finite number of factors inductively.

Proof of uniqueness

#missing/proof

Properties

The Degree operator is given by $𝑑 𝑉 \otimes 𝑊 = 𝑑 𝑉 \otimes 1 + 1 \otimes 𝑑 𝑊$ .

#state/develop | #lang/en | #SemBr