Restricted L_∞-algebras and a derived Milnor-Moore theorem

For every stable presentably symmetric monoidal ∞-category C we use the Koszul duality between the spectral Lie operad and the cocommutative cooperad to construct an enveloping Hopf algebra functor U: AlgLie(C) → Hopf(C) from spectral Lie algebras in C to cocommutative Hopf algebras in C left adjoint to a functor of derived primitive elements. We prove that if C is a rational stable presentably symmetric monoidal ∞-category, the enveloping Hopf algebra functor is fully faithful. We conclude that Lie algebras in C are algebras over the monad underlying the adjunction T U ∘ Lie: C AlgLie(C) → Hopf(C), where Lie is the free Lie algebra and T is the tensor algebra. For general C we introduce the notion of restricted L_∞-algebra as an algebra over the latter adjunction. For any field K we construct a forgetful functor from restricted Lie algebras in connective $H(K)$-modules to the ∞-category underlying a right induced model structure on simplicial restricted Lie algebras over K.