English
The interaction between gradedComm and gradedMul is coherent: braiding commutes across multiplication in a compatible way.
Русский
Взаимодействие gradedComm и gradedMul согласовано: браидинг переставляет элементы при умножении согласованно.
LaTeX
$$$$ gradedComm_R(\mathcal{A},\mathcal{B})(gradedMul_R(\mathcal{A},\mathcal{B})(x,y)) = gradedMul_R(gradedComm_R(\mathcal{A},\mathcal{B})(x), gradedComm_R(\mathcal{A},\mathcal{B})(y)). $$$$
Lean4
theorem gradedComm_gradedMul (x y : DirectSum _ 𝒜 ⊗[R] DirectSum _ ℬ) :
gradedComm R 𝒜 ℬ (gradedMul R 𝒜 ℬ x y) = gradedMul R ℬ 𝒜 (gradedComm R 𝒜 ℬ x) (gradedComm R 𝒜 ℬ y) :=
by
suffices
(gradedMul R 𝒜 ℬ).compr₂ (gradedComm R 𝒜 ℬ).toLinearMap =
(gradedMul R ℬ 𝒜 ∘ₗ (gradedComm R 𝒜 ℬ).toLinearMap).compl₂ (gradedComm R 𝒜 ℬ).toLinearMap
from LinearMap.congr_fun₂ this x y
ext i₁ a₁ j₁ b₁ i₂ a₂ j₂ b₂
dsimp
rw [gradedComm_of_tmul_of, gradedComm_of_tmul_of, tmul_of_gradedMul_of_tmul]
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specialize `map_smul` to avoid timeouts.
simp_rw [Units.smul_def, ← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, LinearMap.map_smul, LinearMap.smul_apply]
simp_rw [Int.cast_smul_eq_zsmul R, ← Units.smul_def, DirectSum.lof_eq_of, DirectSum.of_mul_of, ←
DirectSum.lof_eq_of R, gradedComm_of_tmul_of, tmul_of_gradedMul_of_tmul, smul_smul, DirectSum.lof_eq_of, ←
DirectSum.of_mul_of, ← DirectSum.lof_eq_of R]
simp_rw [← uzpow_add, mul_add, add_mul, mul_comm i₁ j₂]
congr 1
abel_nf
rw [two_nsmul, uzpow_add, uzpow_add, Int.units_mul_self, one_mul]
