Formalisation of the Category of Hopf Algebras in Lean4

Hopf algebras are used in various areas of mathematics and theoretical physics, such as algebraic geometry and quantum groups. In this article, we formalise a few basic results about Hopf algebras. In particular, we prove that the set of R-algebra homomorphisms \({{\,\textrm{Hom}\,}}_R(A, L)\) from a commutative R-Hopf algebra A to a commutative R-algebra L can be endowed with a group structure under the convolution product. Furthermore, we also formalise an anti-equivalence between the category of commutative R-Hopf algebras and the category of affine group schemes over R, where the latter is defined as group objects of corepresented functors from commutative R-algebras to \({\textsf{Set}}\) .