English
The graded multiplication is associative with the braiding, i.e., grading-aware rearrangements satisfy associativity up to graded commutativity.
Русский
Градуированное умножение ассоциативно совместимо с браидингом: перестановки с учётом градации удовлетворяют ассоциативности с учётом graded commutativity.
LaTeX
$$$$ gradedComm_R(\mathcal{A},\mathcal{B})(gradedMul_R(\mathcal{A},\mathcal{B})(x,y), z) = gradedMul_R( x, gradedComm_R(\mathcal{A},\mathcal{B})(y,z) ). $$$$
Lean4
theorem gradedMul_algebraMap (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) (r : R) :
gradedMul R 𝒜 ℬ x (algebraMap R _ r ⊗ₜ 1) = r • x :=
by
suffices (gradedMul R 𝒜 ℬ).flip (algebraMap R _ r ⊗ₜ 1) = DistribMulAction.toLinearMap R _ r by
exact DFunLike.congr_fun this x
ext
dsimp
erw [tmul_of_gradedMul_of_tmul]
rw [mul_zero, uzpow_zero, one_smul, smul_tmul', mul_one, _root_.Algebra.smul_def, Algebra.commutes]
rfl
