Primitive elements in a Hopf algebra

Facts about primitive elements in a Hopf algebra.

Main declarations

• Bialgebra.IsPrimitiveElem.antipode_eq_neg: the antipode sends primitive elements to their negation.
• Bialgebra.IsPrimitiveElem.antipode: the antipode preserves primitivity.

References

• D. Grinberg, V. Reiner, Hopf algebras in combinatorics

@[simp]

theorem Bialgebra.IsPrimitiveElem.antipode_eq_neg {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [HopfAlgebra R A] {a : A} (ha : IsPrimitiveElem R a) : (HopfAlgebraStruct.antipode R) a = -a

See Proposition 1.4.17 in [GR20].

theorem Bialgebra.IsPrimitiveElem.antipode {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [HopfAlgebra R A] {a : A} (ha : IsPrimitiveElem R a) : IsPrimitiveElem R ((HopfAlgebraStruct.antipode R) a)

theorem Bialgebra.IsPrimitiveElem.antipode_antipode {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [HopfAlgebra R A] {a : A} (ha : IsPrimitiveElem R a) : (HopfAlgebraStruct.antipode R) ((HopfAlgebraStruct.antipode R) a) = a