Hopf algebra morphisms

Mathlib defines morphisms in HopfAlgCat R to be bialgebra morphisms; the missing algebraic fact is that such a morphism automatically preserves the antipode. We prove that here by the uniqueness of inverses in the convolution monoid.

Main results

• BialgHomClass.coe_comp_antipode: a bialgebra morphism between Hopf algebras commutes with the antipodes as underlying linear maps.
• BialgHomClass.map_antipode: a bialgebra morphism between Hopf algebras commutes with the antipodes, pointwise.

References

The proof uses Mathlib's convolution product on linear maps, due to Yaël Dillies, Michał Mrugała and Yunzhou Xie.

@[simp]

theorem BialgHomClass.coe_comp_antipode {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebra R B] [FunLike F A B] [BialgHomClass F R A B] (φ : F) : ↑φ ∘ₗ HopfAlgebraStruct.antipode R = HopfAlgebraStruct.antipode R ∘ₗ ↑φ

A bialgebra-hom-like map between Hopf algebras commutes with the antipodes, as a statement about underlying linear maps.

@[simp]

theorem BialgHomClass.map_antipode {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebra R B] [FunLike F A B] [BialgHomClass F R A B] (φ : F) (a : A) : φ ((HopfAlgebraStruct.antipode R) a) = (HopfAlgebraStruct.antipode R) (φ a)

A bialgebra-hom-like map between Hopf algebras commutes with the antipodes, pointwise.