Are there (enough) injectives in condensed abelian groups? The question is very simple : does $Cond(\mathbf{Ab})$, the category of condensed abelian groups (as defined in Scholze's Lectures in Condensed Mathematics), have enough injectives ?
Does it, in fact, have any nontrivial injective ?
Recall that $Cond(\mathbf{Ab})$ is defined to be the colimit over strong limit cardinals $\kappa$ of $Sh(*_{\kappa-proet}, \mathbf{Ab})$, where $*_{\kappa-proet}$ is the site of $\kappa$-small profinite sets (it's easier to just use extremally disconnected spaces, and it is in fact equivalent)
Each of these sheaf-categories has enough injectives, but it's not clear that the colimit does, because a priori, the left Kan extension functor (along the inclusion of $\kappa$-small extremally disconnected  spaces to $\kappa'$-small ones)  $Sh(*_{\kappa-proet}, \mathbf{Ab}) \to Sh(*_{\kappa'-proet}, \mathbf{Ab})$ ($\kappa<\kappa'$) has no reason to preserve injectives, and any injective comes from one of these categories.
A lot of the time one can do without actual injectives (for instance to define $R\hom$, use projectives; or you can also a lot of time use the injectives of one of the sheaf-categories to get what you need), but I suspect that they might be useful at some point; and the question seems relevant regardless
One could argue that we don't care about set-theoretic complications but it seems to me that this is one situation where they're actually non-stupid complications (that can't be solved by just saying "fix a universe"), but maybe someone can explain why they don't matter here ?
EDIT : in this comment, Scholze seems to claim that there are not enough injectives : he says "A few things that exist in pyknotic condensed sets but not in condensed abelian groups (e.g., injective pyknotic abelian groups)". So the question could become : what would be a proof of that ?
 A: Indeed, there are no nonzero injective condensed abelian groups.
Let $I$ be an injective condensed abelian group. We can find some surjection
$$ \bigoplus_{j\in J} \mathbb Z[S_j]\to I$$
for some index set $J$ and some profinite sets $S_j$, where $\mathbb Z[S_j]$ is the free condensed abelian group on $S_j$ -- this is true for any condensed abelian group. But now we can find an injection
$$\bigoplus_{j\in J} \mathbb Z[S_j]\hookrightarrow K$$
into some compact abelian group $K$, for example a product of copies of $\mathbb Z_p$ for any chosen prime $p$. Indeed, it suffices to do this for any summand individually (embedding into a product in the end), and each factor embeds into a product of copies of $\mathbb Z$ (by choosing many maps $S\to \mathbb Z$), thus into a product of copies of $\mathbb Z_p$.
We remark that it is in this step that we need to work in the condensed setting: In the pyknotic setting, $J$ can be larger than the relevant cutoff cardinal for the profinite sets, so $K$ would not be in the site of $\kappa$-small compact Hausdorff spaces.
By injectivity of $I$, we get a surjection $K\to I$. In particular, the underlying condensed set of $I$ is quasicompact.
Now assume that $I$ is $\kappa$-condensed for some $\kappa$, and pick a set $A$ of cardinality bigger than $\kappa$, and consider the injection
$$\bigoplus_A I\hookrightarrow \prod_A I.$$
The sum map $\bigoplus_A I\to I$ extends to $\prod_A I\to I$ by injectivity of $I$.
I claim that the map $\prod_A I\to I$ necessarily factors over a map $\prod_{A'} I\to I$ for some subset  $A'\subset A$ where the cardinality of $A'$ is less than $\kappa$. To check this, we use the surjection $K\to I$; then it is enough to prove that the map $\prod_A K\to I$ factors over $\prod_{A'} K\to I$ for some such $A'$. But this follows from $I$ being $\kappa$-condensed and $\prod_A K$ being profinite.
Thus, the sum map $\bigoplus_A I\to I$ factors over $\prod_{A'} I\to I$ for some $A'\subset A$. But then restricting the sum map along the inclusion $I\to \bigoplus_A I$ given by some $a\in A\setminus A'$ gives both the identity and the zero map, finally showing that $I=0$.
I hope I didn't screw something up.
A: If I understand Peter Scholze's answer correctly, a key feature of the category of condensed abelian groups is that from any projective object P there is a monomorphism to a compact projective object Q. The same argument applies to other condensed abelian categories such as the category of condensed vector spaces over a given finite field.
