A derived Milnor-Moore theorem

For every stable presentably symmetric monoidal ∞ ∞ -category C C and every non-unital ∞ ∞ -operad O O in C C , where "Equation missing" , we construct a Koszul duality adjunction aligned TQO: AlgO(C) CoalgO⁽C): PrimOaligned TQ O : Alg O ( C ) ⇆ Coalg O ∨ ( C ) : Prim O between O O -algebras in C C and coalgebras over the Koszul dual ∞ ∞ -cooperad of O O . We prove that if all norm maps in C C associated to symmetric groups are equivalences, the unit of Koszul duality X → PrimO(TQO(X)) X → Prim O ( TQ O ( X ) ) identifies with the canonical map X → X^ := lim n ≥ 1τ ₙ(O) ∘ OX X → X ∧ : = lim n ≥ 1