English
If A and B are coalgebras, then their tensor product A ⊗_R B inherits a coalgebra structure defined by comul = AlgebraTensorModule.tensorTensorTensorComm ∘ (comul ∘ comul) and counit = rid ∘ map counit counit.
Русский
Если A и B — коалгебры, то их тензорное произведение наследует коалгебраическую структуру: копуляция = tensorTensorTensorComm ∘ (comul ∘ comul) и counit = rid ∘ map counit counit.
LaTeX
$$$\mathrm{comul}_{A\otimes B} = \mathrm{AlgebraTensorModule.tensorTensorTensorComm} \circ \mathrm{AlgebraTensorModule.map}(\mathrm{comul},\mathrm{comul}),\\ \mathrm{counit}_{A\otimes B} = \mathrm{AlgebraTensorModule.rid} \circ \mathrm{AlgebraTensorModule.map}(\mathrm{counit},\mathrm{counit}).$$$
Lean4
@[simp]
theorem lid_symm_apply (a : P) : (Coalgebra.TensorProduct.lid R P).symm a = 1 ⊗ₜ a :=
rfl
