English
The MonoidAlgebra A[G] is equipped with a Hopf algebra structure, in particular its antipode and comultiplication are defined compatibly with the group G and the algebra A.
Русский
MonoidAlgebra A[G] оснащается структурой HopfAlgebra, в частности antipode и комульптация определены совместно с G и A.
LaTeX
$$$\text{MonoidAlgebra.instHopfAlgebraStruct }\;\Rightarrow\; \text{HopfAlgebra } R\,(A[G]).$$$
Lean4
instance instHopfAlgebra : HopfAlgebra R (MonoidAlgebra A G)
where
mul_antipode_rTensor_comul := by
ext a b : 2
simpa [← (ℛ R b).eq] using congr(lsingle (R := R) (1 : G) $(sum_antipode_mul_eq_algebraMap_counit (ℛ R b)))
mul_antipode_lTensor_comul := by
ext a b : 2
simpa [← (ℛ R b).eq] using congr(lsingle (R := R) (1 : G) $(sum_mul_antipode_eq_algebraMap_counit (ℛ R b)))
