Affine group schemes of finite type are antiequivalent to finitely generated commutative Hopf algebras

(Part (a), the functor.) For an affine group scheme $G$ of finite type over $k$, [F1] makes $\mathcal{O}(G)$ a commutative Hopf algebra, finitely generated by [F2]; for a morphism $f\text{\hspace{0.17em}⁣}:G\to H$ of group schemes, [F1] makes $\mathcal{O}(f)\text{\hspace{0.17em}⁣}:\mathcal{O}(H)\to \mathcal{O}(G)$ a morphism of Hopf algebras, and $\mathcal{O}$ of composites and identities is computed by pullback, giving the contravariant functor.

(Part (b), the group scheme.) Let $A$ be a finitely generated commutative Hopf algebra over $k$. By [F3] the maps $\mathrm{\Delta },\epsilon ,S$ have comorphisms $m=\mathrm{Spec}\mathrm{\Delta }\text{\hspace{0.17em}⁣}:\mathrm{Spec}A{\times }_k\mathrm{Spec}A\to \mathrm{Spec}A$, $e=\mathrm{Spec}\epsilon \text{\hspace{0.17em}⁣}:\mathrm{Spec}k\to \mathrm{Spec}A$ and $i=\mathrm{Spec}S\text{\hspace{0.17em}⁣}:\mathrm{Spec}A\to \mathrm{Spec}A$, using $\mathrm{Spec}(A{\otimes }_{k}A)\cong \mathrm{Spec}A{\times }_k\mathrm{Spec}A$. Reversing the argument of The coordinate ring of an affine group scheme is a commutative Hopf algebra turns the coassociativity, counit and antipode axioms into $m\circ (m\times \mathrm{id})=m\circ (\mathrm{id}\times m)$, $m\circ (e\times \mathrm{id})=\mathrm{id}=m\circ (\mathrm{id}\times e)$ and $m\circ (i,\mathrm{id})=e\circ p=m\circ (\mathrm{id},i)$, because the comorphism of $m\times \mathrm{id}$ is $\mathrm{\Delta }\otimes \mathrm{id}$ and $\mathcal{O}$ is a functor; hence $\mathrm{Spec}A$ is a group scheme over $k$. It is of finite type: the identity chart exhibits $k\to A$ as finitely generated, and the structure morphism is quasi-compact because affine schemes are quasi-compact (Every affine scheme is quasi-compact).

(Part (a), full faithfulness.) The functor is the restriction of the fully faithful anti-equivalence of [F3] to group objects and cogroup objects with structure-preserving morphisms: a scheme morphism $f\text{\hspace{0.17em}⁣}:G\to H$ is a group-scheme morphism exactly when it satisfies $f\circ m_G=m_H\circ (f\times f)$, $f\circ e_G=e_H$, $i_H\circ f=f\circ i_G$ (Morphisms and closed subgroup schemes of group schemes), and passing to comorphisms this is exactly the condition that $\mathcal{O}(f)$ preserves $\mathrm{\Delta }$, $\epsilon$, $S$; the bijection on Hom-sets is inherited from [F3], so the functor is full and faithful.

(Part (b), inverse constructions.) Starting from a finitely generated commutative Hopf algebra $A$, the coordinate Hopf algebra of $\mathrm{Spec}A$ is $(\mathrm{\Gamma }(\mathrm{Spec}A,\mathcal{O}),\mathcal{O}(m),\mathcal{O}(e),\mathcal{O}(i))\cong (A,\mathrm{\Delta },\epsilon ,S)$ by [F3] and [F4], so the round trip recovers $A$ up to isomorphism. Starting from an affine group scheme $G$ of finite type, [F3] gives $\mathrm{Spec}\mathcal{O}(G)\cong G$ and the transposition of the group identities identifies the reconstructed group structure with the original one, so the round trip recovers $G$ up to isomorphism.

(Antiequivalence and choice.) Steps 2.1 and 2.2 show that $G\mapsto \mathcal{O}(G)$ is fully faithful and essentially surjective onto finitely generated commutative Hopf algebras, with quasi-inverse $A\mapsto \mathrm{Spec}A$; hence it is an antiequivalence of categories. AC was used in [F2] for finite generation and in step 1.2 for affine quasi-compactness. The group-object construction, compatibility of morphisms and round-trip isomorphisms are formal consequences of the affine anti-equivalence.