The finite dual is a coalgebra and descends through bialgebras and Hopf algebras

If $f\in A^{\circ }$ vanishes on a finite-codimensional two-sided ideal $I$, and $g\in A^{\circ }$ vanishes on such an ideal $J$, then $f,g$ and every linear combination vanish on $I\cap J$. The map $A\mathrm{/}(I\cap J)\to A\mathrm{/}I\oplus A\mathrm{/}J$, $a+(I\cap J)\mapsto (a+I,a+J)$, is injective, so its image is a subspace of a finite-dimensional vector space and is finite-dimensional by [F2]. Thus $A^{\circ }$ is a vector subspace.

Let $q:A\to A\mathrm{/}I$ be the quotient map and write $f=\bar{f}q$. Since $A\mathrm{/}I$ is finite-dimensional, [F3] identifies $((A\mathrm{/}I)\otimes (A\mathrm{/}I){)}^{\ast }$ with $(A\mathrm{/}I{)}^{\ast }\otimes (A\mathrm{/}I{)}^{\ast }$; the transpose of multiplication on $A\mathrm{/}I$ therefore gives a finite tensor ${\sum }_i{\bar{f}}_i\otimes {\bar{g}}_i$ with $\bar{f}((a+I)(b+I))={\sum }_i{\bar{f}}_i(a+I){\bar{g}}_i(b+I)$. Pulling the factors back along $q$ yields ${\mathrm{\Delta }}^{\circ }(f)={\sum }_i({\bar{f}}_{i}q)\otimes ({\bar{g}}_{i}q)\in A^{\circ }\otimes A^{\circ }$, and its evaluation on $a\otimes b$ is $f(ab)$.

If $f(a)=\mathrm{\ell }(\rho (a)v)$ is a coefficient of a finite-dimensional representation $\rho :A\to {\mathrm{End}}_k(V)$, then $\ker \rho$ is a two-sided ideal of finite codimension and $f(\ker \rho )=0$, so $f\in A^{\circ }$. Conversely, if $f$ vanishes on a finite-codimensional ideal $I$, the finite-dimensional quotient $V=A\mathrm{/}I$ is a left $A$-module by $a\cdot (b+I)=ab+I$; the vector $v=1+I$ and functional $\mathrm{\ell }(b+I)=f(b)$ are well-defined and satisfy $f(a)=\mathrm{\ell }(a\cdot v)$. Thus the finite-dual functionals are exactly the finite-dimensional matrix coefficients.

The evaluation map $A^{\ast }\otimes A^{\ast }\to (A\otimes A{)}^{\ast }$ is injective: write a finite tensor as ${\sum }_{i=1}^r{\varphi }_i\otimes {\psi }_i$ with the ${\varphi }_i$ linearly independent, by choosing a basis of the finite span of its first factors and rewriting. The map $A\to k^r$, $a\mapsto ({\varphi }_1(a),\dots ,{\varphi }_r(a))$, is surjective, since a proper subspace of the finite-dimensional space $k^r$ has a nonzero annihilating linear functional, which would give a nontrivial dependence among the ${\varphi }_i$. Choose $a_j$ mapping to the $j$-th standard vector; if the tensor evaluates to zero on every $a\otimes b$, then ${\psi }_j(b)=0$ for every $b$ and every $j$, so the tensor is zero. Therefore the tensor characterized in step 1.2 is independent of the chosen ideal $I$.

For coefficients $f(a)=\mathrm{\ell }(\rho (a)v)$ and $g(a)=\mu (\sigma (a)w)$ of finite-dimensional representations on $V,W$, define $(\rho \otimes \sigma )(a\otimes b)=\rho (a)\otimes \sigma (b)$. By [F6], this is well-defined; on pure tensors it preserves products because $(\rho (a{a}^{\mathrm{\prime }})\otimes \sigma (b{b}^{\mathrm{\prime }}))=(\rho (a)\rho (a^{\mathrm{\prime }})\otimes \sigma (b)\sigma (b^{\mathrm{\prime }}))=(\rho (a)\otimes \sigma (b))(\rho (a^{\mathrm{\prime }})\otimes \sigma (b^{\mathrm{\prime }}))$, and it preserves the unit. Composing with the unital algebra map ${\mathrm{\Delta }}_H$ from [F4] gives a finite-dimensional unital representation. Its coefficient at $\mathrm{\ell }\otimes \mu ,v\otimes w$ is $\sum f(h_1)g(h_2)=(f\ast g)(h)$, so convolution preserves $H^{\circ }$.

If $f(a)=\mathrm{\ell }(\rho (a)v)$, define an action on $V^{\ast }$ by $(h\cdot \lambda )(v^{\mathrm{\prime }})=\lambda (\rho (S_H(h))v^{\mathrm{\prime }})$. By [F5], $S_H(h{h}^{\mathrm{\prime }})=S_H(h^{\mathrm{\prime }})S_H(h)$, whence $(h\cdot (h^{\mathrm{\prime }}\cdot \lambda ))(v^{\mathrm{\prime }})=\lambda (S_H(h^{\mathrm{\prime }})S_H(h)v^{\mathrm{\prime }})=((h{h}^{\mathrm{\prime }})\cdot \lambda )(v^{\mathrm{\prime }})$, and the unit acts as the identity. The coefficient of this finite-dimensional representation at vector $\mathrm{\ell }\in V^{\ast }$ and functional ${\mathrm{ev}}_v(\lambda )=\lambda (v)$ is $f(S_H(h))$. Therefore $S_H^{\ast }(f)\in H^{\circ }$.

For $f\in A^{\circ }$, evaluation of $({\mathrm{\Delta }}^{\circ }\otimes \mathrm{i}\mathrm{d}){\mathrm{\Delta }}^{\circ }(f)$ and $(\mathrm{i}\mathrm{d}\otimes {\mathrm{\Delta }}^{\circ }){\mathrm{\Delta }}^{\circ }(f)$ on $a\otimes b\otimes c$ gives $f((ab)c)$ and $f(a(bc))$, equal by associativity. The evaluation map on three finite tensor factors is injective by repeating the finite-independent-family argument of step 2.1. Evaluating $({\epsilon }^{\circ }\otimes \mathrm{i}\mathrm{d}){\mathrm{\Delta }}^{\circ }(f)$ and $(\mathrm{i}\mathrm{d}\otimes {\epsilon }^{\circ }){\mathrm{\Delta }}^{\circ }(f)$ at $a$ gives $f(1_{A}a)=f(a)=f(a{1}_A)$, so these maps are the identity.

The functional ${\epsilon }_H$ lies in $H^{\circ }$: its kernel is a two-sided ideal, and the induced map $H\mathrm{/}\ker {\epsilon }_H\to k$ is injective by definition of the kernel and surjective since ${\epsilon }_H(1_H)=1$. The two counit equations for $H$ show that it is the left and right convolution unit on $H^{\circ }$. Convolution is associative on $H^{\circ }$: by step 2.2 its products stay in $H^{\circ }$, and because the bialgebra hypothesis gives a coassociative coproduct, for $f,g,r\in H^{\circ }$ and $h\in H$ we have $((f\ast g)\ast r)(h)={\sum }_{(h)}f(h_1)g(h_2)r(h_3)=(f\ast (g\ast r))(h)$; the finite Sweedler contractions are well-defined by [F7]. The coproduct ${\mathrm{\Delta }}^{\circ }(f)$ is a finite tensor by step 1.2. For $f,g\in H^{\circ }$ and $a,b\in H$, ${\mathrm{\Delta }}^{\circ }(f\ast g)(a\otimes b)=(f\ast g)(ab)=\sum f(a_1{b}_1)g(a_2{b}_2)=({\mathrm{\Delta }}^{\circ }(f){\mathrm{\Delta }}^{\circ }(g))(a\otimes b)$, because [F4] makes ${\mathrm{\Delta }}_H$ an algebra map. By the tensor-evaluation injectivity of step 2.1, this proves coproduct multiplicativity. Also ${\mathrm{\Delta }}^{\circ }({\epsilon }_H)={\epsilon }_H\otimes {\epsilon }_H$ since ${\epsilon }_H(ab)={\epsilon }_H(a){\epsilon }_H(b)$, and the counit is multiplicative since $(f\ast g)(1_H)=(f\otimes g)({\mathrm{\Delta }}_H(1_H))=f(1_H)g(1_H)$. Thus the convolution product is associative and unital, and all bialgebra identities hold.

Write ${\mathrm{\Delta }}^{\circ }(f)={\sum }_i{f}_i\otimes g_i$, so ${\sum }_i{f}_i(a)g_i(b)=f(ab)$. Then ${\sum }_i(S_H^{\ast }{f}_i\ast g_i)(h)={\sum }_{(h)}f(S_H(h_1)h_2)={\epsilon }_H(h)f(1_H),$ and ${\sum }_i(f_i\ast S_H^{\ast }{g}_i)(h)={\sum }_{(h)}f(h_1{S}_H(h_2))={\epsilon }_H(h)f(1_H)\mathrm{.}$ These are the two antipode equations for $S_H^{\ast }$ in $H^{\circ }$, by [F5]. Thus the finite dual of every Hopf algebra is Hopf, without an inverse $S_H^{-1}$.