instHopfAlgebraStruct — Mathlib

English

The AddMonoidAlgebra A[G] carries a Hopf algebra structure with antipode defined via sums over group elements with signs, compatible with the addition group structure.

Русский

AddMonoidAlgebra A[G] получает структуру HopfAlgebra с antipode, определяемым через суммы по элементам группы с признаком и совместимостью с операцией сложения.

LaTeX

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

Lean4

instance instHopfAlgebraStruct : HopfAlgebraStruct R A[G] where
  antipode := Finsupp.lsum R fun g => Finsupp.lsingle (-g) ∘ₗ antipode R

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