English
For x ∈ A and y ∈ B, the comultiplication on x ⊗ y equals the tensor-product commutativity map applied to comul x and comul y; i.e., comul(x ⊗ y) = tensorTensorTensorComm( comul x, comul y ).
Русский
Для x ∈ A, y ∈ B копуляция на x ⊗ y равна применению tensorTensorTensorComm к копуляциям элементов: comul(x ⊗ y) = tensorTensorTensorComm( comul x, comul y ).
LaTeX
$$$\mathrm{comul}(x \otimes y) = \mathrm{AlgebraTensorModule.tensorTensorTensorComm}(R,S,R,S,A,A,B,B) (\mathrm{comul}\,x \otimes_? \mathrm{comul}\,y).$$$
Lean4
/-- The associator for tensor products of R-coalgebras, as a coalgebra equivalence. -/
protected noncomputable def assoc : (M ⊗[S] N) ⊗[R] P ≃ₗc[S] M ⊗[S] (N ⊗[R] P) :=
{ AlgebraTensorModule.assoc R S S M N P with
counit_comp := by ext; simp
map_comp_comul := by
ext x y z
dsimp
hopf_tensor_induction comul (R := S) x with x₁ x₂
hopf_tensor_induction comul (R := S) y with y₁ y₂
hopf_tensor_induction comul (R := R) z with z₁ z₂
simp }
