English
Let R be a commutative ring and M, N, P be coalgebras over R. The comultiplication on the tensor object obtained by first tensoring M and N and then tensoring with P (via the canonical associativity) coincides with the standard comultiplication on the triple tensor M ⊗_R N ⊗_R P, i.e. the two constructions give the same coalgebra structure up to the canonical associativity isomorphism.
Русский
Пусть R — коммутативное кольцо, а M, N, P — коалгебры над R. Расщепление (коалгебраическое отображение раздвоения) на тензорном объекте, полученном сначала из M и N, затем с P (через каноническую ассоциативность), совпадает с обычным коалгебральным распадом на M ⊗_R N ⊗_R P; т.е. две конструирования дают одну и ту же структуру коалгебры (с учётом канонического тензорного изъяна).
LaTeX
$$$\operatorname{comul} (R := R) (A := ((\mathrm{CoalgCat}.of R M \otimes \mathrm{CoalgCat}.of R N) \otimes \mathrm{CoalgCat}.of R P : \mathrm{CoalgCat\, R})) = \operatorname{comul} (A := M \otimes[R] N \otimes[R] P)$$$
Lean4
theorem comul_tensorObj_tensorObj_left :
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]
dsimp
simp only [toComonObj]
simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def, AlgebraTensorModule.tensorTensorTensorComm_eq]
rfl
