English
For homogeneous elements a ∈ 𝒜_i, b ∈ ℬ_j, the graded commutator map gradedCommAux applied to lof on (i,j)(a⊗b) equals the graded swap up to a sign: gradedCommAux(lof(i,j)(a⊗b)) = (-1)^{ij} lof(j,i)(b⊗a).
Русский
Для однородных элементов a ∈ 𝒜_i, b ∈ ℬ_j, отображение gradedCommAux, применённое к lof на (i,j)(a⊗b), равно graded swap с множителем (-1)^{ij: степени}: gradedCommAux(lof(i,j)(a⊗b)) = (-1)^{ij} lof(j,i)(b⊗a).
LaTeX
$$$\\operatorname{gradedCommAux}(R,\\mathcal{A},\\mathcal{B})\\bigl(\\operatorname{lof}(R,\\mathcal{A},\\mathcal{B})(i,j)(a\\otimes b)\\bigr) = (-1)^{ij}\\, \\operatorname{lof}(R,\\mathcal{B},\\mathcal{A})(j,i)(b\\otimes a)$$$
Lean4
@[simp]
theorem gradedCommAux_lof_tmul (i j : ι) (a : 𝒜 i) (b : ℬ j) :
gradedCommAux R 𝒜 ℬ (lof R _ 𝒜ℬ (i, j) (a ⊗ₜ b)) = (-1 : ℤˣ) ^ (j * i) • lof R _ ℬ𝒜 (j, i) (b ⊗ₜ a) :=
by
rw [gradedCommAux]
simp [mul_comm i j]
