Is there a good theory of solid vector spaces? Lately I have become interested in solid $F$-modules where $F$ is some discrete field. Ideally, one would want a category that is as nicely behaved as solid abelian groups or solid $\mathbb{F_p}$-modules.
I have managed to show that a discrete field is a solid module over itself, so we get that the usual $\prod_I F$ are all solid, which seems like a promising start. However, I have been unsuccessful in trying to show that one gets an abelian category.
If one tries to mimic the proof that solid abelian groups are an abelian category, the main obstruction we run into is $\operatorname{RHom}_F (\prod_I F, F)$. This is quite a difficult computation, and the main tool used to do this with condensed abelian groups is the short exact sequence $0 \to \mathbb{Z} \to  \mathbb{R} \to \mathbb{R}/\mathbb{Z} \to 0$ so that we can use cohomology, but we don't have a similar sequence for $F$-modules.
The proof strategy for the analogue statement in $\mathbb{F}_p$-modules is heavily reliant on the fact that $\mathbb{F}_p$ is finite.
Essentially, the proof one needs is that $F_\blacksquare$ is an analytic ring. I know from Scholze's notes that it is suspected not all discrete rings form an analytic ring but I was hoping that this might be true for fields.
So my question is: should we expect a good theory of solid $F$-modules and why/why not?
EDIT: Some more details about my question. I am interested in whether $F_\blacksquare$ is analytic, where $F[S]^\blacksquare = \varprojlim F[S_i]$.
The motivation for this is a bit convoluted, but I'm in a situation where having the $\prod_I F$ as compact projective generators of an abelian category would be particularly convenient in order to extend certain functors only defined on these compact projective generators.
 A: I will prove that the result is true if $F$ is a finitely generated field, but fails if $F$ is countably generated field that is not finitely generated.
Let me first discuss the case $F=\mathbb Q$. For $F=\mathbb Q$, one has the idempotent solid $\mathbb Z$-algebra $\hat{\mathbb Z}=\mathrm{lim}_n \mathbb Z/n\mathbb Z$ (where $n$ runs over nonzero integers). One can form the Bousfield localization of $D(\mathbb Z_\blacksquare)$ that kills all $\hat{\mathbb Z}$-modules. As a Bousfield localization, this can also be described as a full subcategory of $D(\mathbb Z_\blacksquare)$ in terms of the corresponding local objects; and one computes that the localization of $\mathbb Z_\blacksquare[S] = \mathrm{lim}_i \mathbb Z[S_i]$ is $\mathrm{lim}_i \mathbb Q[S_i]$ (as the quotient $\mathrm{lim}_i \mathbb Q/\mathbb Z[S_i]$ is a module over $\hat{\mathbb Z}$, while $\hat{\mathbb Z}$ has no maps to $\mathbb Q$, and thus no maps $\mathrm{lim}_i \mathbb Q[S_i]$). This easily implies that $\mathbb Q$ with $\mathbb Q_\blacksquare[S] = \mathrm{lim}_i \mathbb Q[S_i]$ defines an analytic ring.
If $F$ is any finitely generated field, write it as the field of fractions of some domain $R$ that is a finitely generated $\mathbb Z$-algebra. Then $R_\blacksquare$ exists as an analytic ring, and one can form the idempotent $R_\blacksquare$-algebra $\hat{R}=\mathrm{lim}_f R/f$, where $f$ runs over nonzero elements of $R$. Passing to the corresponding Bousfield localization,  the localization of $\mathrm{lim}_i R[S_i]$ is $\mathrm{lim}_i K[S_i]$, from which one gets the desired result.
Now assume that $F$ is not finitely generated, but still countably generated. I claim that
$$\mathrm{Ext}^1_F(\prod_{\mathbb N} F,F)\neq 0,$$
where the $\mathrm{Ext}^1$ is computed in condensed $F$-modules; but if $F_\blacksquare$ was an analytic ring then such Ext-groups would have to be zero.
Write $F$ as a sequential colimit of finitely generated fields $F_n$. By writing $R\mathrm{Hom}_F$ as $R\mathrm{lim}_n R\mathrm{Hom}_{F_n}$ and a lim-lim^1-sequence, it suffices to show that
$$ \mathrm{lim}^1 \mathrm{Hom}_{F_n}(\prod_{\mathbb N} F,F)\neq 0.$$
But one can show that any morphism of condensed abelian groups $\prod_{\mathbb N} F\to F$ factors over a finite product, hence it suffices that
$$ \mathrm{lim}^1 (\bigoplus_{\mathbb N} \mathrm{Hom}_{F_n}(F,F))\neq 0.$$
But for any tower $(X_n)_n$ of abelian groups, one has $\mathrm{lim}^1(\bigoplus_{\mathbb N} X_n)\neq 0$ as long as $(X_n)_n$ does not satisfy the Mittag-Leffler condition (see I. Emmanouil. Mittag-Leffler condition and the vanishing of lim^1. Topology, 35(1):267–271, 1996). But if the $F_n$ are strictly increasing, $\mathrm{Hom}_{F_n}(F,F)$ forms a strictly decreasing chain of abelian groups.
It is likely that the result fails for any $F$ that is not finitely generated; I did not try to think about this.
