English
The comultiplication on the tensor product is given by the tensor product of the comultiplications followed by the tensor strength.
Русский
Комульпликация на тензорном произведении задаётся как тензорная карта комуль и затем тензорная сила.
LaTeX
$$$Δ[A \otimes B] = (Δ[A] ⊗ₘ Δ[B]) ≫ tensorμ A A B B$$$
Lean4
/-- The comultiplication on the tensor product of two comonoids is
the tensor product of the comultiplications followed by the tensor strength
(to shuffle the factors back into order).
-/
@[simp]
theorem tensorObj_comul (A B : C) [ComonObj A] [ComonObj B] : Δ[A ⊗ B] = (Δ[A] ⊗ₘ Δ[B]) ≫ tensorμ A A B B :=
by
rw [tensorObj_comul']
congr
simp only [tensorμ, unop_tensorObj, unop_op]
apply Quiver.Hom.unop_inj
dsimp [op_tensorObj, op_associator]
rw [Category.assoc, Category.assoc, Category.assoc]
