English
A preliminary equality for the comultiplication on a tensor product: Δ[A ⊗ B] equals (Δ[A] ⊗ₘ Δ[B]) followed by the unop of tensorμ.
Русский
Предварительное равенство для комульпликации на тензорном произведении: Δ[A ⊗ B] = (Δ[A] ⊗ₘ Δ[B]) ≫ (tensorμ (op A) (op B) (op A) (op B)).unop
LaTeX
$$$Δ[A \otimes B] = (Δ[A] \otimes_m Δ[B]) \;≫\; (tensorμ (op A) (op B) (op A) (op B)).unop$$
Lean4
/-- Preliminary statement of the comultiplication for a tensor product of comonoids.
This version is the definitional equality provided by transport, and not quite as good as
the version provided in `tensorObj_comul` below.
-/
theorem tensorObj_comul' (A B : C) [ComonObj A] [ComonObj B] :
Δ[A ⊗ B] = (Δ[A] ⊗ₘ Δ[B]) ≫ (tensorμ (op A) (op B) (op A) (op B)).unop := by rfl
