English
For a Hopf algebra H = (R,A) and any a ∈ A, the map mul' applied to the rTensor of antipode with the comultiplication on a equals the algebra map sending a to counit(a) times 1: mul'(R,A)((antipode R) rTensor (Coalgebra.comul a)) = algebraMap(R,A)(Coalgebra.counit a).
Русский
Для гепф-алгебры H и любого a ∈ A выполняется тождество: умножение после применения антиподы к rTensor(comul(a)) даёт алгебраическое умножение counit(a) на единицу.
LaTeX
$$$\mathrm{mul}'\,R\,A\bigl((\mathrm{antipode}\,R)\,\mathrm{rTensor}\, (\mathrm{Coalgebra}.comul\ a)\bigr) = \mathrm{algebraMap}\,R\,A\bigl(\mathrm{Coalgebra}.counit\ a\bigr).$$$
Lean4
@[simp]
theorem mul_antipode_rTensor_comul_apply (a : A) :
LinearMap.mul' R A ((antipode R).rTensor A (Coalgebra.comul a)) = algebraMap R A (Coalgebra.counit a) :=
LinearMap.congr_fun mul_antipode_rTensor_comul a
