Completion of the classifying stack $BG$ at a point With the classifying stack $BG$ I have come across "the formal completion of $BG$ at point", which is denoted $\widehat{BG}$, for instance on page 7 of https://arxiv.org/pdf/1703.08578.pdf, but I cannot find a reference for the definition.
My questions are:

*

*What is the definition of $\widehat{BG}$?


*Does the definition arise naturally with a morphism $p: \widehat{BG} \to BG$?


*In the case of yes to 2, is this morphism finite? What is $p_{*}{\mathcal{O}_{\widehat{BG}}}$?
 A: I'm definitely not the right person to answer that, but hopefully Cunningham's Law will do its thing. You might also want to have a look at Pavel's answer to a somewhat related question of mine
My naive understanding is that it should be the formal stack (e.g. in this sense) controlled by the DG coalgebra $CE(\mathfrak g)$. In other words this is the quotient of a point by the formal group scheme associated with $G$, as it should of course.
A (probably more general) point of view is that it controls de formal derived moduli problem associated with $\mathfrak g$ seen as a DG Lie algebra, in the sense of Lurie and Pridham. As far as I understand it means it represents the functor mapping a "small" augmented commutative algebra $A$ (roughly the $E_\infty$ version of a local $k$-algebra with residue field $k$, I guess) to $Hom_{Lie}(D(A), \mathfrak g)$ where $D$ is the Koszul dual Lie algebra functor. Another reference is this survey where this particular example is mentioned as a motivation, though not quite worked out in details I suppose.
I'm fairly sure there is always such a map $p$, and at least if $G$ is smooth $p_*$ should be the "rationalization" functor, i.e. the right adjoint of the inclusion
$$
Rep\ G \longrightarrow Rep\ \mathfrak g.$$
