English
For homogeneous components a in 𝒜_i and b in ℬ_j, the graded commutativity on tmul gives a sign (-1)^{ji} when swapping order.
Русский
Для однородных компонентов a в 𝒜_i и b в ℬ_j, градуированная браидинг-коммутативность даёт знак (-1)^{ji} при перестановке местами.
LaTeX
$$$$ gradedComm_R(\mathcal{A},\mathcal{B})(a_i \otimes b_j) = (-1)^{ji} (b_j \otimes a_i). $$$$
Lean4
theorem gradedComm_of_tmul_of (i j : ι) (a : 𝒜 i) (b : ℬ j) :
gradedComm R 𝒜 ℬ (lof R _ 𝒜 i a ⊗ₜ lof R _ ℬ j b) = (-1 : ℤˣ) ^ (j * i) • (lof R _ ℬ _ b ⊗ₜ lof R _ 𝒜 _ a) :=
by
rw [gradedComm]
dsimp only [LinearEquiv.trans_apply, LinearEquiv.ofLinear_apply]
rw [TensorProduct.directSum_lof_tmul_lof, gradedCommAux_lof_tmul, Units.smul_def,
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 specialized `map_smul` to `LinearEquiv.map_smul` to avoid timeouts.
← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, TensorProduct.directSum_symm_lof_tmul, Int.cast_smul_eq_zsmul, ←
Units.smul_def]
