instHopfAlgebraStruct — Mathlib

English

There is a Hopf algebra structure on the MonoidAlgebra A[G], given by a defined antipode that uses the inverses in G and the antipode on A.

Русский

Существует структура HopfAlgebra на MonoidAlgebra A[G], задаваемая antipode через инверсии в G и antipode на A.

LaTeX

$$$\text{MonoidAlgebra}.\text{instHopfAlgebraStruct }(R,A,G)\;:\; \text{HopfAlgebra } R\,(A[G]).$$$

Lean4

instance instHopfAlgebraStruct : HopfAlgebraStruct R (MonoidAlgebra A G) where
  antipode := Finsupp.lsum R fun g => Finsupp.lsingle g⁻¹ ∘ₗ antipode R

Похожие утверждения