Convolution inverses in a commutative Hopf algebra

Let A be a commutative Hopf algebra with antipode S. For every algebra map f from A into a commutative algebra, f ∘ S is a left convolution inverse of f; mathlib's convolution group AlgHom.convGroup states this only when the target is itself a bialgebra. In the convolution group WithConv (A →ₐ[R] A) the antipode S is the inverse of the identity, S ∘ S is the inverse of S, and so S ∘ S is the identity.

Main results

• AlgHom.comp_antipode_cancel: (f ∘ S) ⋆ f = 1.
• HopfAlgebra.antipode_antipode: the antipode is an involution.

[UPSTREAM] Belongs in Mathlib/RingTheory/HopfAlgebra/Convolution.lean, settling the TODO on commutative Hopf algebras in Mathlib/RingTheory/HopfAlgebra/Basic.lean.

References

• [GR20]

theorem AlgHom.comp_antipode_cancel {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring C] [Algebra R C] (f : A →ₐ[R] C) : WithConv.toConv (f.comp (HopfAlgebra.antipodeAlgHom R A)) * WithConv.toConv f = 1

For an algebra map f from a commutative Hopf algebra into a commutative algebra, f ∘ S is a left convolution inverse of f: the antipode law S ⋆ id = 1 transported along f.

theorem HopfAlgebra.antipodeAlgHom_comp_antipodeAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : (antipodeAlgHom R A).comp (antipodeAlgHom R A) = AlgHom.id R A

@[simp]

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

See Corollary 1.4.12 in [GR20].

theorem HopfAlgebra.antipode_involutive {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : Function.Involutive ⇑(antipode R)