English
Graded multiplication is associative when combined with braiding, i.e., a(xy) = (xa)y under grading rules.
Русский
Градуированное умножение ассоциативно совмещается с браидингом: a(xy) = (xa)y с учётом градации.
LaTeX
$$$$ gradedMul_R(gradedMul_R(x,y), z) = gradedMul_R(x, gradedMul_R(y,z)). $$$$
Lean4
theorem gradedMul_assoc (x y z : DirectSum _ 𝒜 ⊗[R] DirectSum _ ℬ) :
gradedMul R 𝒜 ℬ (gradedMul R 𝒜 ℬ x y) z = gradedMul R 𝒜 ℬ x (gradedMul R 𝒜 ℬ y z) :=
by
let mA := gradedMul R 𝒜 ℬ
suffices
LinearMap.llcomp R _ _ _ mA ∘ₗ mA =
(LinearMap.llcomp R _ _ _ LinearMap.lflip.toLinearMap <| LinearMap.llcomp R _ _ _ mA.flip ∘ₗ mA).flip
by exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z
ext ixa xa ixb xb iya ya iyb yb iza za izb zb
dsimp [mA]
simp_rw [tmul_of_gradedMul_of_tmul, Units.smul_def, ← Int.cast_smul_eq_zsmul R, LinearMap.map_smul₂,
LinearMap.map_smul, DirectSum.lof_eq_of, DirectSum.of_mul_of, ← DirectSum.lof_eq_of R, tmul_of_gradedMul_of_tmul,
DirectSum.lof_eq_of, ← DirectSum.of_mul_of, ← DirectSum.lof_eq_of R, mul_assoc]
simp_rw [Int.cast_smul_eq_zsmul R, ← Units.smul_def, smul_smul, ← uzpow_add, add_mul, mul_add]
congr 2
abel
