Algebraic K-theory "with proper support" I would like to know what is the "correct" algebraic $K$-theory "with proper support". I suppose that the answer should be found in the condensed world, which is mostly inspired the existence of six functors. See Lectures on Condensed Mathematics, Appendix to Lecture VIII.
$\DeclareMathOperator\Tor{Tor}\DeclareMathOperator\Perf{Perf}\DeclareMathOperator\Spec{Spec}$More precisely, given a map $f\colon R\to S$ of finitely generated rings, we have the functor $f_!\colon D(S_\blacksquare)\to D(R_\blacksquare)$ of "direct image with proper support" which preserves small colimits. Suppose that $f$ is of finite $\Tor$-amplitude, then $f_!$ induces a functor $\Perf(S_\blacksquare)\to\Perf(R_\blacksquare)$ between compact objects in $D(S_\blacksquare)$ and $D(R_\blacksquare)$ respectively. The ordinary $K$-theoretic machinery leads to a map $K(\Perf(S_\blacksquare))\to K(\Perf(R_\blacksquare))$ which looks like some kind of "integral along fibers" of $\Spec S\to\Spec R$ for compactly supported cohomologies. However, this does not seem to be satisfactory, since both sides are discrete.
One way to get a condensed structure might be the following: $\Perf(R_\blacksquare)$ (resp. $\Perf(S_\blacksquare)$) should be a "condensed stable symmetric monoidal $\infty$-category". There might be set-theretic issues, but let's ignore them for a moment. Take the maximal groupoid, we get a map of condensed $E_\infty$-monoids and taking the group completion, we get a map of condensed spectra.
Edit: I was mistaken, we should pass to the Waldhausen $S_\bullet$ construction for this, but seemingly this could also be equipped with a condensed structure.
It is not immediately clear whether these spectra are solid. Is there alternative characterizations of these condensed spectra, hopefully without reference to "condensed $\infty$-categories"?
On the other hand, there is a concept of condensed $K$-theory in Lectures on Analytic Geometry, Prop 10.6. However, this does not seem to coincide with the construction above.
Update: As Denis-Charles Cisinski pointed out, the approach sketched above does not work since the corresponding $K$-theory is trivial by Eilenberg's Swindle applied to the infinite product). It is not immediate for me what is a replacement, in view of the compactly supported topological $K$-theory, for example.
 A: Actually, the possibility of defining such a thing was one of my motivations for studying this condensed mathematics in the first place.  That said, the story is far from complete.
First, I guess a reasonable definition is the following.  For $R\rightarrow S$ a map of finitely generated commutative rings, recall that there is an idempotent commutative algebra object $S_{\infty/R}$ in derived solid $(S,R)$-modules such that modules over $S_{\infty/R}$ are exactly those modules which die on localization to solid $S$-modules.  For example, if $S=R[t]$ then $S_{\infty/R}=R((t^{-1}))$, but in general $S_{\infty/R}$ lives in several cohomological degrees.  Now the K-theory wth proper support should be the homotopy fiber of
$$K(S)\rightarrow K(S_{\infty/R}).$$
However, this leaves open the question of how $K(S_{\infty/R})$ should be defined.  one could do it naively by just taking perfect complexes, but this leads to a messy theory.  Peter Scholze and I realized that the correct way to define such K-theory is instead to take the continuous K-theory, in the sense of Efimov, of a certain dualizable category of modules which contains, but is bigger than, the ind-category of perfect complexes.  This is the category of nuclear modules briefly described in Analytic.pdf.
This probably defines what is the "correct" object.  That said, I view this actual definition as unsatisfactory, because I would like a natural dualizable category of modules whose continuous K-theory directly gives the K-theory with proper supports.  I don't know how to do this; the best I've managed so far is one that gives the suspension.
Another thing I'd like to mention is that the reason I was interested in this K-theory with proper supports is that it shows up in the approach I worked out to Artin maps, https://arxiv.org/abs/1703.07842 .  If $R$ is a finite type $\mathbb{Z}$-algebra, the source of the Artin map as I define it is the K-theory of the category of $R$-modules in $D^b(LCA)$, the bounded derived category of locally compact abelian groups.  If $R$ is a regular $\mathbb{F}_p$-algebra, I conjecture that this K-theory is equivalent to the suspension of the compactly supported K-theory of $R$ over $\mathbb{Z}$ in the above sense, if you interpret $K(S_{\infty/R})$ in the naive way with perfect complexes.  By the way, the hypotheses on $R$ are not crucial: one can remove the regularity assumption by working with G-theory, and the $\mathbb{F}_p$-algebra assumption by adding in the appropriate archimedean part at $\infty$ as well.  When $R$ is one-dimensional I believe these conjectures have been proved (though with slightly different definitions) by Braunling, https://arxiv.org/abs/1710.10819 .
