Hopf algebra morphisms

This file records Hopf-algebra API needed for the affine-group-scheme dictionary in the reductive-groups roadmap. 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 usual convolution-inverse uniqueness argument.

Main results

• BialgHom.toLinearMap_comp_antipode and BialgHom.map_antipode: a bialgebra morphism between Hopf algebras commutes with the antipodes (the convolution-inverse identities themselves are Mathlib's LinearMap.antipode_mul_id and LinearMap.id_mul_antipode, and the pure-tensor antipode formula is Mathlib's simp lemma TensorProduct.antipode_def).

References

This supplies a formal prerequisite for the Tau Ceti reductive-groups roadmap, Layer 0, "the functor of points and the three-way dictionary": morphisms in the Hopf-algebra model must respect the inverse map in the affine group-scheme model. The proof uses Mathlib's convolution product on linear maps, due to Yaël Dillies, Michał Mrugała and Yunzhou Xie. The pure-tensor antipode formula is Mathlib's TensorProduct.antipode_def in Mathlib.RingTheory.HopfAlgebra.TensorProduct, imported where consumed.

theorem TauCeti.BialgHom.toLinearMap_comp_antipode {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebra R B] (φ : A →ₐc[R] B) : φ.toLinearMap ∘ₗ HopfAlgebraStruct.antipode R = HopfAlgebraStruct.antipode R ∘ₗ φ.toLinearMap

A bialgebra morphism between Hopf algebras commutes with the antipodes, as a statement about underlying linear maps.

theorem TauCeti.BialgHom.map_antipode {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebra R B] (φ : A →ₐc[R] B) (a : A) : φ ((HopfAlgebraStruct.antipode R) a) = (HopfAlgebraStruct.antipode R) (φ a)

A bialgebra morphism between Hopf algebras commutes with the antipodes, pointwise.

@[simp]

theorem TauCeti.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.