English
Let M, N, P be coalgebras over a commutative ring R. The coalgebra structure on the nested tensor product CoalgCat.of R M ⊗ (CoalgCat.of R N ⊗ CoalgCat.of R P) agrees, under the canonical identification with the triple tensor product M ⊗[R] (N ⊗[R] P), with the standard coalgebra structure on M ⊗[R] (N ⊗[R] P). In other words, the comultiplication on the left-hand side coincides with the comultiplication on the right-hand side via the natural associativity identifications.
Русский
Пусть M, N, P — коалgebры над коммутативным кольцом R. Структура копулирования на вложенном тензорном произведении CoalgCat.of R M ⊗ (CoalgCat.of R N ⊗ CoalgCat.of R P) совпадает с обычной структурой копуляции на тройном тензорном произведении M ⊗[R] (N ⊗[R] P) через естественные композиции ассоциативности.
LaTeX
$$$\operatorname{Coalgebra}.\operatorname{comul}(R := R,\ A := (CoalgCat.of R M \otimes (CoalgCat.of R N \otimes CoalgCat.of R P) : CoalgCat R)) = \operatorname{Coalgebra}.\operatorname{comul}(A := M \otimes[R] (N \otimes[R] P))$$$
Lean4
theorem comul_tensorObj_tensorObj_right :
Coalgebra.comul (R := R) (A := (CoalgCat.of R M ⊗ (CoalgCat.of R N ⊗ CoalgCat.of R P) : CoalgCat R)) =
Coalgebra.comul (A := M ⊗[R] (N ⊗[R] P)) :=
by
rw [ofComonObjCoalgebraStruct_comul]
simp only [Comon.monoidal_tensorObj_comon_comul]
simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def, AlgebraTensorModule.tensorTensorTensorComm_eq]
rfl
