The fundamental theorem of coalgebras

If $C$ is finite-dimensional, take $D=C$. Now assume $C$ is arbitrary and use [A1]. It is enough first to put a single $c\in C$ into a finite-dimensional subcoalgebra; when $c=0$, take $D=0$ with the unique maps ${\mathrm{\Delta }}_D:0\to 0\otimes 0$ and ${\epsilon }_D:0\to k$. The coalgebra identities hold because the identity map on $0$ is zero and all maps with domain $0$ are zero, and the inclusion $D\hookrightarrow C$ preserves $\mathrm{\Delta }$ and $\epsilon$ because both composites from $0$ are zero.

Let $c\mathrm{\ne }0$. By [F1], write $\mathrm{\Delta }(c)={\sum }_{j=1}^r{x}_j\otimes y_j$ and let $Y=\mathrm{span}(y_1,\dots ,y_r)$. By [F3] choose a finite ordered basis $b_1,\dots ,b_n$ of $Y$. Since $\mathrm{\Delta }(c)\mathrm{\ne }0$ by the counit equation in [F2], $n\ge 1$. By [F8], write each $y_j={\sum }_{i=1}^n{\lambda }_{ij}{b}_i$ and regroup the finite tensor sum to obtain $\mathrm{\Delta }(c)={\sum }_{i=1}^n{a}_i\otimes b_i$, where $a_i={\sum }_{j=1}^r{\lambda }_{ij}{x}_j$; the $b_i$ are independent.

Set $A=\mathrm{span}(a_1,\dots ,a_n)$ and let $q:C\to C\mathrm{/}A$. In the common iterated tensor product $C\otimes (C\otimes C)$, coassociativity [F2] gives ${\sum }_i\alpha (\mathrm{\Delta }(a_i)\otimes b_i)={\sum }_i{a}_i\otimes \mathrm{\Delta }(b_i)$. Apply $q\otimes \mathrm{i}\mathrm{d}\otimes \mathrm{i}\mathrm{d}$ and naturality of $\alpha$; the right-hand side vanishes because $q(a_i)=0$, so, using the associator to regard each term in $((C\mathrm{/}A)\otimes C)\otimes C$, ${\sum }_i((q\otimes \mathrm{i}\mathrm{d})\mathrm{\Delta }(a_i))\otimes b_i=0$. Apply the tensor symmetry that exchanges the two factors $((C\mathrm{/}A)\otimes C)$ and $C$ to obtain ${\sum }_i{b}_i\otimes ((q\otimes \mathrm{i}\mathrm{d})\mathrm{\Delta }(a_i))=0$. Since the $b_i$ are independent, [F5] gives $(q\otimes \mathrm{i}\mathrm{d})\mathrm{\Delta }(a_i)=0$ for every $i$. The kernel identity [F4] therefore gives $\mathrm{\Delta }(a_i)\in A\otimes C$, and linearity gives $\mathrm{\Delta }(A)\subseteq A\otimes C$.

Apply [F3] to the finite spanning list $a_1,\dots ,a_n$; its choice-free finite-list construction gives an ordered basis $e_1,\dots ,e_m$ of $A$. If $A=0$, the expression for $\mathrm{\Delta }(c)$ in step 2.1 gives $\mathrm{\Delta }(c)=0$, so the counit equation in [F2] gives $c=0$, contradicting the hypothesis of step 2.1. Hence $m\ge 1$. Let ${\varphi }_i:A\to k$ be the $i$th coordinate map in this ordered basis. If $x={\sum }_i{r}_i{e}_i$ and $y={\sum }_i{s}_i{e}_i$, uniqueness of coordinates gives ${\varphi }_j(x+y)=r_j+s_j$ and ${\varphi }_j(\lambda x)=\lambda r_j$, so each ${\varphi }_j$ is linear by [F8]. Write $j_A:A\hookrightarrow C$ for the inclusion. By [F4], $j_A\otimes {\mathrm{i}\mathrm{d}}_C$ is injective; since $\mathrm{\Delta }(e_j)$ lies in its image by step 3.1, let $\tilde{\mathrm{\Delta }}(e_j)\in A\otimes C$ be its unique preimage. Define $c_{ij}:={\lambda }_C\circ ({\varphi }_i\otimes {\mathrm{i}\mathrm{d}}_C)(\tilde{\mathrm{\Delta }}(e_j))$, where ${\lambda }_C:k\otimes C\to C$ is the tensor unit map. Writing $\tilde{\mathrm{\Delta }}(e_j)={\sum }_t{x}_t\otimes y_t$ and expanding $x_t={\sum }_i{\varphi }_i(x_t)e_i$ gives $\mathrm{\Delta }(e_j)={\sum }_i{e}_i\otimes {\sum }_t{\varphi }_i(x_t)y_t={\sum }_i{e}_i\otimes c_{ij}$.

Apply coassociativity to $\mathrm{\Delta }(e_j)={\sum }_i{e}_i\otimes c_{ij}$. In $C\otimes (C\otimes C)$ its two sides are the images of ${\sum }_{i,\mathrm{\ell }}{e}_{\mathrm{\ell }}\otimes (c_{\mathrm{\ell }i}\otimes c_{ij})$ and ${\sum }_i{e}_i\otimes \mathrm{\Delta }(c_{ij})$, respectively, under $j_A\otimes {\mathrm{i}\mathrm{d}}_{C\otimes C}:A\otimes (C\otimes C)\to C\otimes (C\otimes C)$, using the associator to identify the first expression with the left coassociativity composite. This tensor map is injective by [F4] and the associator naturality in [F11], so the two displayed preimages are equal in $A\otimes (C\otimes C)$. Apply the well-defined linear map ${\lambda }_{C\otimes C}\circ ({\varphi }_s\otimes {\mathrm{i}\mathrm{d}}_{C\otimes C})$ for each $s$; since ${\varphi }_s(e_{\mathrm{\ell }})={\delta }_{s\mathrm{\ell }}$, it gives $\mathrm{\Delta }(c_{sj})={\sum }_i{c}_{si}\otimes c_{ij}$.

The right counit equation on $e_j$ gives $e_j={\sum }_i{e}_i\epsilon (c_{ij})$, so uniqueness of coordinates [F8] gives $\epsilon (c_{ij})={\delta }_{ij}$. The left counit equation gives $e_j={\sum }_i\epsilon (e_i)c_{ij}$, so each basis vector $e_j$ lies in $D:=\mathrm{span}\{c_{i\mathrm{\ell }}:1\le i,\mathrm{\ell }\le m\}$. Hence $A\subseteq D$.

Let $E_m$ be the finite comatrix coalgebra of [F6] and define the linear map $\mathrm{\Phi }:E_m\to C$ by extending $u_{ij}\mapsto c_{ij}$ from its basis, which is possible by [F13]. Steps 5.1 and 5.2 show on every basis vector that ${\mathrm{\Delta }}_C\mathrm{\Phi }=(\mathrm{\Phi }\otimes \mathrm{\Phi }){\mathrm{\Delta }}_{E_m}$ and ${\epsilon }_C\mathrm{\Phi }={\epsilon }_{E_m}$; linearity makes $\mathrm{\Phi }$ a coalgebra map.

The right counit equation on $c$ gives $c={\sum }_i{a}_i\epsilon (b_i)$. By step 5.2 every $a_i\in A\subseteq D$, so $c\in D$. This places $c$ in the candidate coefficient subspace.

Put $K=\ker \mathrm{\Phi }$. By [F7], $K$ is a coideal, $E_m\mathrm{/}K$ is a coalgebra, and the induced map $\bar{\mathrm{\Phi }}:E_m\mathrm{/}K\to C$ is a coalgebra map. It is injective because $\mathrm{\Phi }(x)=0$ exactly when $x\in K$, and its image is $D$. Regard it as a linear isomorphism $\psi :E_m\mathrm{/}K\to D$, and define ${\mathrm{\Delta }}_D=(\psi \otimes \psi ){\mathrm{\Delta }}_{E_m\mathrm{/}K}{\psi }^{-1}$ and ${\epsilon }_D={\epsilon }_{E_m\mathrm{/}K}{\psi }^{-1}$. For coassociativity, composing the two coalgebra composites on $D$ with the surjection $\psi$ gives respectively $(\psi \otimes (\psi \otimes \psi ))\alpha ({\mathrm{\Delta }}_{E_m\mathrm{/}K}\otimes \mathrm{i}\mathrm{d}){\mathrm{\Delta }}_{E_m\mathrm{/}K}$ and $(\psi \otimes (\psi \otimes \psi ))(\mathrm{i}\mathrm{d}\otimes {\mathrm{\Delta }}_{E_m\mathrm{/}K}){\mathrm{\Delta }}_{E_m\mathrm{/}K}$, which are equal by coassociativity on $E_m\mathrm{/}K$ and naturality of the associator [F11]. Similarly, composing the left and right counit composites with $\psi$ gives $\psi {\lambda }_{E_m\mathrm{/}K}(\epsilon \otimes \mathrm{i}\mathrm{d})\mathrm{\Delta }$ and $\psi {\rho }_{E_m\mathrm{/}K}(\mathrm{i}\mathrm{d}\otimes \epsilon )\mathrm{\Delta }$, both equal to $\psi$; surjectivity of $\psi$ proves the two counit equations on $D$. Since $\bar{\mathrm{\Phi }}=j_D\psi$ is a coalgebra map, ${\mathrm{\Delta }}_C{j}_D\psi =(j_D\otimes j_D)(\psi \otimes \psi ){\mathrm{\Delta }}_{E_m\mathrm{/}K}=(j_D\otimes j_D){\mathrm{\Delta }}_D\psi$ and ${\epsilon }_C{j}_D\psi ={\epsilon }_D\psi$; surjectivity of $\psi$ proves that the inclusion $j_D:D\hookrightarrow C$ is a coalgebra map. Thus $D$ is a subcoalgebra by [F12]. Its finite spanning list of $m^2$ coefficients makes it finite-dimensional by [F3], and together with step 6.2 it contains $c$.

For a finite set $S$, apply the one-element assertion to each $c\in S$ and take the sum of the resulting subcoalgebras. By [F7] the sum is a subcoalgebra; it contains $S$ and is spanned by the finite union of their finite coefficient lists, so [F3] makes it finite-dimensional. If $S=\mathrm{\varnothing }$, take the zero subcoalgebra.

The finite-dimensional case is choice-free by step 1.1. In the arbitrary-dimensional case, [A1] is used through the coefficient-separation and tensor-kernel suppliers in step 3.1 and through the quotient and sum results in steps 7.1 and 7.2; steps 2.1 and 4.1 use only finite tensor expressions and the choice-free finite-list basis lemma. Step 7.1 proves the one-element case, and step 7.2 handles the finite subset, including the empty set.