Cartier's theorem: affine group schemes in characteristic zero are smooth

Smoothness. By [F1] the module ${\mathrm{\Omega }}_{G\mathrm{/}k}$ is free, hence locally free, and $G$ is locally of finite type over $k$ by [F6]; the field $k$ has characteristic $0$, so [F2] applies and the structure morphism $G\to \mathrm{Spec}k$ is smooth.

Necessity of characteristic zero. Let $p>0$ and let $A=k[s]\mathrm{/}(s^p)$, with class $s\mathrm{\ne }0$ and $s^p=0$ by [F5]; its localisation $R=A_{(s)}$ at the maximal ideal $(s)$ is a nonzero local ring in which $s\mathrm{/}1$ is again a nonzero nilpotent, since an element killing $s$ in $A$ lies in the annihilator $(s^{p-1})\subseteq (s)$. If $\mathrm{Spec}A$, the underlying scheme of ${\alpha }_p$, were smooth at the origin, [F3] applied with the trivial extension $K=k$ would make $R$ a regular local ring, and [F4] would make $R$ a domain, contradicting $(s\mathrm{/}1{)}^p=0$ with $s\mathrm{/}1\mathrm{\ne }0$. Hence ${\alpha }_p$ is not smooth; by the substitution of [F5] the scheme of ${\mu }_p$ has the same local ring at the origin, so ${\mu }_p$ is not smooth either, and the characteristic-zero hypothesis in the theorem cannot be dropped.

Regularity and reducedness. Let $g\in G$. By the definition of smoothness, $G\to \mathrm{Spec}k$ is smooth at $g$, so the fibre over $(0)\in \mathrm{Spec}k$ is geometrically regular at $g$; taking the trivial field extension $K=k\mathrm{/}k$, [F3] says that the local ring ${\mathcal{O}}_{G,g}$ is regular. Since a regular local ring is a domain by [F4], every ${\mathcal{O}}_{G,g}$ has no nonzero nilpotent, so $G$ is reduced.

Conclusion. Step 1.1 proves that an affine group scheme of finite type over a field of characteristic $0$ is smooth over that field; step 2.1 derives regularity of all local rings and reducedness; step 1.2 shows that the hypothesis is essential. The Axiom of Choice is used only through the cited criterion [F2] and the regularity suppliers [F3, F4].