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](https://golem.ph.utexas.edu/category/2020/03/pyknoticity_versus_cohesivenes.html#c057620), 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 ?



Are there (enough) injectives in condensed abelian groups?
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.


