Question 1.Is a correct proof of Leray's theorem (the one that says that a connected graded Hopf algebra $H$ over a field of characteristic $0$ is isomorphic as an algebra to the symmetric algebra $\operatorname*{Sym}\left( H^{+}/\left( H^{+}\right) ^{2}\right) $, where $H^{+}=\operatorname*{Ker} \epsilon$ is the kernel of the counit $\epsilon$ of $H$) contained in any version of the famous article "On the structure of Hopf algebras" by Milnor and Moore?

Question 2.What are the currently existing sources for Leray's theorem?

**Detailed version.** One of the earliest, and still most influential, papers
on Hopf algebras is the article "On the structure of Hopf algebras" by Milnor
and Moore. It exists in two versions:

I am interested in the following theorem, which I shall call *Leray's theorem*
despite being utterly confused about its provenance (possibly Hopf, Samelson
and Borel have some claims here as well -- any help with the history?):

Leray's theorem.Let $\mathbf{k}$ be a commutative $\mathbb{Q}$-algebra. Let $H$ be a graded Hopf algebra over $\mathbf{k}$ (in the modern meaning of this word -- i.e., it has to have an associative multiplication $m$, a unit $u$, a coassociative comultiplication $\Delta$, a counit $\epsilon$, and an antipode $S$; and all these maps are graded). Assume that $H$ is connected (i.e., the $0$-th graded component of $H$ is isomorphic to $\mathbf{k}$) and commutative (i.e., all $a,b\in H$ satisfy $ab=ba$). Let $H^{+} =\operatorname*{Ker}\epsilon$ be the kernel of the counit $\epsilon :H\rightarrow\mathbf{k}$ of $H$. Then, $H\cong\operatorname*{Sym}\left( H^{+}/\left( H^{+}\right) ^{2}\right) $ as graded $\mathbf{k}$-algebras.

From what I understand, Milnor and Moore claim to prove this theorem in the particular case when $\mathbf{k}$ is a field. Specifically, it appears to follow from Theorem 4.6 in [A] and from Theorem 7.5 in [B].

(Notice that the notations in [A] are different from mine. In particular, associativity and coassociativity are not required by default from Hopf algebras, but rather required only when explicitly stated. If they wouldn't require $\mathbf{k}$ to be a field, their results would hence be more general than what I call Leray's theorem. Also notice that they are using the notations $I\left( H\right) $ for $H^{+}$, as well as $Q\left( H\right) $ for $\mathbf{k}\otimes_{H}H^{+}\cong H^{+}/\left( H^{+}\right) ^{2}$, and finally $A\left( V\right) $ for the symmetric algebra $\operatorname*{Sym} V$, at least when we are working with evenly graded algebras.)

What I don't understand is how they prove all this. Their proof relies on a lemma (Lemma 4.3 in [A], resp. Proposition 4.17 in [B]), which states (at least in the particular case we care about) that in the situation of Leray's theorem, if we further assume that $\mathbf{k}$ is a field, the natural morphism $\left\{ \text{primitive elements of }H\right\} \rightarrow H^{+}/\left( H^{+}\right) ^{2}$ (which is well-defined since primitive elements of $H$ always lie in $H^{+}$) is a monomorphism. In other words, the only primitive element in $\left( H^{+}\right) ^{2}$ is $0$. The proof of this lemma relies on some argument where $H$ is assumed to be finitely generated, and then an induction is done on the number of generators, presenting $H$ as a some-sort-of-extension of a Hopf subalgebra $A^{\prime}$ with one less generator by a quotient-of-sorts $A^{\prime\prime}$ with one generator. ("Generator" always mean algebra generator.) This looks highly suspicious to me, since I don't think that Hopf algebras can be deconstructed in such a simple way. I also have never seen arguments like this ever after Milnor's and Moore's work. Thus, the first question: Is it correct?

I am currently writing up my own proof of Leray's theorem, which uses the Eulerian idempotent and is probably common knowledge in the Hopf-combinatorics crowd. Thus, the second question: What should I be referencing?