English
The MonoidAlgebra instance provides a Hopf algebra structure on MonoidAlgebra A G with antipode and comultiplication defined compatibly with the group structure.
Русский
В MonoidAlgebra задаётся структура HopfAlgebra на MonoidAlgebra A G с согласованными антиподом и коумиляцией по структуре группы.
LaTeX
$$$\text{MonoidAlgebra.instHopfAlgebraStruct }(R,A,G) : \text{HopfAlgebra } R\,(MonoidAlgebra A G).$$$
Lean4
instance instHopfAlgebra : HopfAlgebra R A[G]
where
mul_antipode_rTensor_comul := by
ext a b : 2
simpa [← (ℛ R b).eq, single_mul_single] using
congr(lsingle (R := R) (0 : G) $(sum_antipode_mul_eq_algebraMap_counit (ℛ R b)))
mul_antipode_lTensor_comul := by
ext a b : 2
simpa [← (ℛ R b).eq, single_mul_single] using
congr(lsingle (R := R) (0 : G) $(sum_mul_antipode_eq_algebraMap_counit (ℛ R b)))
