English
The braiding is the fundamental isomorphism that switches the two factors in a tensor product of externally graded algebras, introducing a sign depending on degrees.
Русский
Браидинг — это основная изоморфия, которая переставляет две факторы в тензорном произведении внешне-градуированных алгебр, вводя знак в зависимости от степеней.
LaTeX
$$$$\text{gradedComm}: (\bigoplus_i \mathcal{A}_i) \otimes_R (\bigoplus_j \mathcal{B}_j) \cong_R (\bigoplus_j \mathcal{B}_j) \otimes_R (\bigoplus_i \mathcal{A}_i), \quad a\otimes b \mapsto (-1)^{\deg a'\deg b}\; (b\otimes a). $$$$
Lean4
/-- The braiding operation for tensor products of externally `ι`-graded algebras.
This sends $a ⊗ b$ to $(-1)^{\deg a' \deg b} (b ⊗ a)$. -/
def gradedComm : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i) ≃ₗ[R] (⨁ i, ℬ i) ⊗[R] (⨁ i, 𝒜 i) :=
by
refine TensorProduct.directSum R R 𝒜 ℬ ≪≫ₗ ?_ ≪≫ₗ (TensorProduct.directSum R R ℬ 𝒜).symm
exact
LinearEquiv.ofLinear (gradedCommAux _ _ _) (gradedCommAux _ _ _) (gradedCommAux_comp_gradedCommAux _ _ _)
(gradedCommAux_comp_gradedCommAux _ _ _)
