Stable unoriented Thom cohomology is free over the square algebra

Given: AC; the connected bialgebra $\mathcal{A}$ of square operations; the stable Thom cohomology module $M={\widehat{H}}^{\ast }(TO;{\mathbb{F}}_2)$ with its connected coaugmented coalgebra structure and diagonal action; the injective unit orbit $\nu :\mathcal{A}\to M$; and $Q=M\mathrm{/}{\mathcal{A}}^{+}M$.

The bialgebra, the coalgebra and its module-coalgebra compatibility, and the injectivity of the unit orbit are the previously established local results (The admissible square algebra is a connected bialgebra, Stable Thom cohomology is a square-module coalgebra, The zero section proves injectivity of the Thom unit orbit).

The connected graded module-coalgebra freeness theorem applies to these hypotheses and gives $M\cong \mathcal{A}\otimes Q$ with homogeneous bases lifting to free $\mathcal{A}$-bases; the degree pieces of $M$ are finite-dimensional by the degreewise constancy lemma, so the same holds for $Q$ (A connected graded module coalgebra with injective unit orbit is free, Stable universal Thom cohomology is eventually constant in every degree).