Relation between ProCoh and solid modules There are two languages endow the theory of coherent sheaves with a six functor formalism (that I "know" of), one being formulated in $\text{ProCoh}(X)$ by Deligne and the other being $D(\mathcal{O}_{X,\blacksquare})$ of Clausen-Scholze.
I'm curious as to the relation between the two. Every coherent sheaf gives rise to a solid module, and so we have a natural functor
$$\text{Coh}(X)\to D(\mathcal{O}_{X,\blacksquare}).$$
A naive extension of this to a functor $\text{ProCoh}(X)\to D(\mathcal{O}_{X,\blacksquare})$ is given by sending the "limit" of coherent sheaves to the actual limit of their solid modules. Is this the "right" extension to consider?
From the "right" extension you would expect that for any morphism $f:X\to Y$ we have a commutative diagram
$\require{AMScd}$
\begin{CD}
\text{ProCoh}(X) @>>> D(\mathcal{O}_{X,\blacksquare})\\
@V Rf_! V V= @VV f_! V\\
\text{ProCoh}(Y) @>>> D(\mathcal{O}_{Y,\blacksquare}).
\end{CD}
However I've gotten confused by a toy-computation: if $f:\mathbb{A}^1_k\to \text{Spec } k$, $j:\mathbb{A}^1_k\to \mathbb{P}^1_k$, then since $\mathcal{O}_{\mathbb{P}^1_k}$ is an extension of $\mathcal{O}_{\mathbb{A}^1_k}$, we have $j_!\mathcal{O}_{\mathbb{A}^1_k}=''\lim"(\mathcal{O}_{\mathbb{P}^1_k}(-n\infty))_{n}$. In particular
$$R^1f_!\mathcal{O}_{\mathbb{A}^1_k}=\lim_nH^1(\mathbb{P}^1_k,\mathcal{O}_{\mathbb{P}^1_k}(-n\infty))_{n}=\lim_n \left(\frac{1}{x_0x_1}k[\frac{1}{x_0},\frac{1}{x_1}]\right)_{-n}.$$
However, $f_!$ is supposed to respect compact objects, and this does look non-compact. Is my computation wrong or is this indeed compact?
 A: This is a long comment addressing the functor in question but not the lower shriek. I would like to say that it is close to a fully faithful embedding. For example, we claim that the pro-objects in the category of abelian groups of finite presentation (or equivalent, of finite type) is a full subcategory of solid abelian groups.
To see this, let $R=\mathbb Z$. Consider the diagram $\require{AMScd}\newcommand\Ind{\operatorname{Ind}}\newcommand\Pro{\operatorname{Pro}}\newcommand\Perf{\operatorname{Perf}}\newcommand\op{\operatorname{op}}\newcommand\colim{\operatorname{colim}}\newcommand\RHom{\operatorname{RHom}}\newcommand\iRHom{\underline{\operatorname{RHom}}}$
\begin{CD}
\Ind(\Perf_R)^{\op}@>\colim^{\op}>\simeq>D(R)^{\op}\\
@V\simeq VV@VV\iRHom_{R_\blacksquare}(-,R)V\\
\Pro(\Perf_R)@>\lim>>D(R_\blacksquare)
\end{CD}
where the left vertical arrow is induced by the self anti-equivalence $\RHom_R(\cdot,R)\colon\Perf_R^{\op}\to\Perf_R$. The top horizontal arrow is an equivalence since $\Perf_R\subseteq D(R)$ is a set of compact generators. It follows that the bottom functor $\lim$ is fully faithful precisely where the right functor $\iRHom_{R_\blacksquare}(\cdot,R)$ is fully faithful.
We note that the right vertical arrow is fully faithful when restricting to the full subcategory $D^b(R)^{\op}\subseteq D(R)^{\op}$ of bounded objects (which was asked before: Duality between $D^b(\mathbb{Z})$ and $D(\mathrm{Solid})^\omega$). In particular, given a cofiltered diagram of uniformly bounded perfect complexes on the bottom left, since $R=\mathbb Z$ has finite global dimension, the corresponding object on the top left is also uniformly bounded, the result follows.
If I am not mistaken, we only need to assume that $R$ has finite global dimension to make the preceding argument works, and could be slightly strengthened. For example, the restriction of the functor $\iRHom_{R_\blacksquare}(\cdot,R)$ to the full subcategory of bounded above complexes is known to be fully faithful, inducing an anti-equivalence between bounded above complexes and pseudocoherent objects in $D(R_\blacksquare)$ when $R$ has finite global dimension.
