Commit 2023-12-18 04:13 3f7c7ee0

feat: the graded tensor product (#7394) This adds the graded tensor product $A \hat\otimes_R B$, imbued with a multiplication defined on homogeneous tensors by: $$(a \hat\otimes b) \cdot (a' \hat\otimes b') = (-1)^{\deg a' \deg b} (a \cdot a') \hat\otimes (b \cdot b')$$ where $A$ and $B$ are algebras graded by ℕ, ℤ, or ZMod 2 (or more generally, any index that satisfies Module ι (Additive ℤˣ)). We do this in two phases:

• Define bundled morphisms that perform the multiplication and braiding maps on regular tensor products of DirectSums
• Define a new GradedTensorProduct type synonym that attaches the multiplication operator to * notation, and restricts itself to internally-graded algebras.