English
If A is a coalgebra over R, then A^(op) carries a natural coalgebra structure obtained by transporting the comultiplication and counit along the canonical linear equivalence between A and its opposite.
Русский
Если A — коалгебра над R, то у A^op естественная коалгебраическая структура, полученная переносом копулиации и counit вдоль канонического линейного эквивалентности между A и A^op.
LaTeX
$$$A^{op}$ has a coalgebra structure defined by comul_{A^{op}} = map((opLinearEquiv_R).toLinearMap,(opLinearEquiv_R).toLinearMap) \circ\circul \circ (opLinearEquiv_R)^{-1},\; counit_{A^{op}} = counit \circ (opLinearEquiv_R)^{-1} .$$$$
Lean4
noncomputable instance [CoalgebraStruct R A] : CoalgebraStruct R Aᵐᵒᵖ
where
comul :=
map (opLinearEquiv R).toLinearMap (opLinearEquiv R).toLinearMap ∘ₗ comul ∘ₗ (opLinearEquiv R).symm.toLinearMap
counit := counit ∘ₗ (opLinearEquiv R).symm.toLinearMap
