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 ?