English
If A and B are coalgebras with appropriate scalar towers, the tensor product A ⊗_R B is a coalgebra with comul and counit defined by transporting the structure via the canonical tensor-product constructions.
Русский
Если A и B — коалгебры с подходящими скалярами, то A ⊗_R B — коалгебра; копуляция и counit задаются через перенос через канонические конструкции тензорного произведения.
LaTeX
$$$\text{Coalgebra}(S, A \otimes_R B) \text{ with } \mathrm{comul} = \mathrm{AlgebraTensorModule.tensorTensorTensorComm} \circ \mathrm{AlgebraTensorModule.map}(\mathrm{comul},\mathrm{comul}), \; \mathrm{counit} = \mathrm{AlgebraTensorModule.rid} \circ \mathrm{AlgebraTensorModule.map}(\mathrm{counit},\mathrm counit).$$$
Lean4
instance [IsCocomm S A] [IsCocomm R B] : IsCocomm S (A ⊗[R] B) where
comm_comp_comul := by
ext x y
dsimp
conv_rhs => rw [← comm_comul _ x, ← comm_comul _ y]
hopf_tensor_induction comul (R := S) x with x₁ x₂
hopf_tensor_induction comul (R := R) y with y₁ y₂
simp
