English
The comultiplication on the opposite coalgebra A^(op) is the transported comultiplication obtained by conjugating the original comultiplication with the opposite equivalence; explicitly, comul_{A^{op}} = map(opLinearEquiv_R).toLinearMap ∘ comul ∘ (opLinearEquiv_R).symm.toLinearMap.
Русский
Копуляция противоложной коалгебры A^{op} получается путём переноса исходной копуляции через противоположное линейное отображение: comul_{A^{op}} = map(opLinearEquiv_R).toLinearMap ∘ comul ∘ (opLinearEquiv_R)^{-1}.
LaTeX
$$$\mathrm{comul}_{A^{op}} = \mathrm{map}( (\mathrm{opLinearEquiv}_R).toLinearMap, (\mathrm{opLinearEquiv}_R).toLinearMap ) \circ\mathrm{comul} \circ (\mathrm{opLinearEquiv}_R)^{-1}.$$$
Lean4
theorem comul_def [CoalgebraStruct R A] :
comul (R := R) (A := Aᵐᵒᵖ) =
map (opLinearEquiv R).toLinearMap (opLinearEquiv R).toLinearMap ∘ₗ comul ∘ₗ (opLinearEquiv R).symm.toLinearMap :=
rfl
