In his paper where details for Tamarkin's proof of formality are given, Hinich considers a Koszul quadratic operad $P$, a graded $P$-algebra $H$, a $P_\infty$-algebra $X$ with $HX=H$ (as $P$-algebras I presume?) and then gives by HTT a $P_\infty$-algebra structure $Q$ on $H$ so it becomes equivalent to $X$. This is a map $Q : P^{\perp}(H)\to H$ or, what is the same, an element in the Lie algebra $\mathfrak g $ of coderivations of the free $P^{\perp}$-coalgebra $C = P^{\perp}(H)$. This is $\mathbb N$-graded by the arity of $P^{\perp}$.

He wants to prove (Theorem 4.1.3.) that if the inclusion $\mathfrak g_{\geqslant 1} \to \mathfrak g$ induces the zero map on $H^1$, then $H$ is intrinsically formal. In doing so, he uses the notation $C[\lambda]$. I am not sure if this means the 'degree wise' tensor product of $C$ with the polynomial algebra, i.e.

in each degree, this is $C(n)\otimes \lambda^{n-1}$

or the degree wise tensor product of $C$ with a polynomial algebra, i.e.

in each degree, this is $C(n)\otimes \mathbb k[\lambda]$.

Trying to understand the proof of the Theorem 4.1.3., it seems to me it should be the first. This makes sense since the inductive proof in (4.2.6) of page 9 seems to be extending the isotopy $\theta$ 'arity by arity', which is consistent with the first interpretation of the notation. My questions are as follows

- Could someone clarify this?
- In the proof in (4.2.6) Hinich also says ''where $Q'$ is
*some*differential uniquely defined by the above formula'', but I can't figure out what formula he's referring to. Why does $Q'$ exist? - In many lines of paragraph (4.2.6) (second display, fourth display and sixth display equations) Hinich writes $Q$ when I think he means $Q^0$, since after all he wants an isotopy from $C[\lambda]$ with $Q^0$ to $C[\lambda]$ with $Q^\lambda$. Is this the case?