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.
Great question — for some reason this tight relation between extremally disconnected profinite sets and forcing had elapsed me!
I've just been trying to read a bit about it. From what I understand, the sheaf-theoretic approach to forcing, as in MacLane-Moerdijk "Sheaves in geometry and logic" Chapter VI, consists of three steps.
Start with any extremally disconnected profinite set $S$. Consider the category of open and closed subsets of $S$, with the following notion of cover: $\{U_i\subset U\}_i$ is a cover of $U$ if $\bigcup_i U_i\subset U$ is dense in $U$. (This is what, I believe, the "double negation topology" amounts to.) In this topology, the subsheaves of $\ast$ are exactly given by the open and closed subsets $U\subset S$, so one has a boolean topos. The first step is thus completed: The construction of the boolean topos of sheaves $\mathrm{Sh}(S)$ on $S$.
The second step is to pick any point $s\in S$, and take the colimit $\varinjlim_{U\ni s} \mathrm{Sh}(U)$. Here, the subsheaves of $\ast$ are just $\emptyset$ and $\ast$, so it's a boolean topos with only two truth values.
The third step is to start with the topos $\varinjlim_{U\ni s} \mathrm{Sh}(U)$ and somehow make it into a model of ZFC. When I've previously tried myself to contemplate forcing from the sheaf-theoretic point of view, this is the point that got me very confused: In a model of ZFC, elements of sets should be sets, but there's no meaningful way to talk about elements of objects in this topos, and certainly they won't be objects of this topos. I have to read more about this step; MacLane-Moerdijk cite work of Fourman. Apparently the idea is to redo the iterative construction of $V_\alpha$'s by iteratively taking the powerset, but now internally in this topos. [Edit: This third step deals with the problem of turning a structural set theory into a material set theory. A very nice discussion of this is in the paper Comparing material and structural set theories of Shulman. In particular, he explains how to very cleanly go back and forth between models of ECTS + a structural form of replacement, which $\varinjlim_{U\ni s} \mathrm{Sh}(U)$ satisfies, and models of ZFC, see Corollary 9.5.] (I might at this point be sold on structural set theory — forcing seems to have an extremely clean formulation in terms of structural set theory, namely just $\varinjlim_{U\ni s} \mathrm{Sh}(U)$. Please correct me if I'm misunderstanding something!)
In any case, the third step seems to be orthogonal to the question at hand. More salient is that the category of sheaves on $S$ is actually incompactible with the category of sheaves on $S$ that we would consider, where covers are just open covers. This is critical! If $S$ is the Stone-Cech compactification of a discrete set $S_0$, then sheaves in our sense are equivalent to functors on subsets of $S_0$, taking finite disjoint unions to products. But in the forcing-sense, they are equivalent to such functors taking all disjoint unions to products; equivalently, they are just sheaves on the discrete $S_0$. Most condensed sets of interest (like $\mathbb Z$ or $\mathbb R$) do not have this property; actually, the condition singles out the compact Hausdorff condensed sets if I'm not mistaken.
So even before analyzing the question of how to put this together for varying $S$, I think there are slightly different things happening even for individual $S$. But I agree that it's definitely worth finding out if there's something more to this!
Addendum in response to Mike Shulman's question in the comments below: I think $\varinjlim_{U\ni s} \mathrm{Sh}(U)$ is well-pointed. The key seems to be the following: If $f: B\to A$ is a map in $\mathrm{Sh}(S)$ that is surjective in the stalk at $s$, then $f|_U$ is surjective for some $U$ containing $s$. (This property does seem surprising to me. Is it a formal consequence of being a boolean topos?) To prove this, we prove that if $f|_U$ is not surjective for all such $U$, then also $f$ is not surjective in the stalk at $s$. Look at pairs $(V\subset S,a\in A(V))$ of an open and closed subset $V\subset S$ and a section $a$ of $A$ over $V$, such that $a\times_{A|_V} B|_V=\emptyset$. There is an obvious partial order on such; by Zorn's lemma and as any section over a union $\bigcup_i V_i$ extends to the closure by the notion of covering, there is some maximal such $(V,a)$. If $s\in V$, then in particular $f$ is not surjective on the stalk at $s$, as desired. Otherwise, let $U=S\setminus V$, which contains $s$. By assumption, $f|_U$ is not surjective, so there is some $U'\subset U$ and $a'\in A(U')$ such that $a'\times_{A|_{U'}} B|_{U'}$ (a subsheaf of $\ast|_{U'}$) is not all of $\ast|_{U'}$, and thus given by $\ast_{U''}$ for some $U''\subsetneq U'$; replacing $U'$ by $U'\setminus U''$, we can assume that $a'\times_{A|_{U'}} B|_{U'}=\emptyset$. But then $(V\sqcup U',a\sqcup a')$ extends $(V,a)$, contradicting maximality of $(V,a)$.
Best Answer
Some comments:
Regarding 1): They are quite different. Johnstone actually uses a very general notion of "cover" in his sequential topos -- his site is a full subcategory of metrizable profinite sets (=$\aleph_1$-small profinite sets=countable limits of finite sets=sequential Pro-category of finite sets), but not all of his covers are covers in the condensed/pyknotic sense. I'm not sure the more general covers he allows are of much relevance for his positive results, but they preclude his topos from having enough points. (All the other choices have enough points.) It also means that the generating object $\mathbb N\cup\{\infty\}$ is not actually a quasicompact object in his topos.
So a better comparison would be between the version of Johnstone's topos that restricts to the finitary covers.
This admits a geometric morphism from $\aleph_1$-condensed sets.(Edit (Nov 14, 2023): It doesn't: Pullback does not preserve finite limits. One can correct this by enlarging the defining site of Johnstone's topos to include all closed subsets of $(\mathbb N\cup \{\infty\})^n$, for all $n$.) Now $\aleph_1$-condensed sets actually admit a description very similar to this version of Johnstone's topos, but replacing $\mathbb N \cup \{\infty\}$ with the Cantor set, which is the universal metrizable profinite set (i.e. surjects onto any other). But the Cantor set is much bigger than $\mathbb N\cup\{\infty\}$! This has some important consequences, for example $[0,1]$ is quasicompact in $\aleph_1$-condensed sets, but very much fails to be so in Johnstone's topos. Such quasicompactness is used all over the place in our arguments. For example, an extremely important property is the following:You can consider CW complexes as ($\aleph_1$-)condensed sets. Now any topos has its inherent notion of cohomology, so you can take the resulting cohomology of CW complexes. Then, in the condensed world:
I believe this would fail in Johnstone's topos (correct me if I'm wrong!). (Edit (Nov 14, 2023): I believe in the version of Johnstone's topos sketched above, using all closed subsets of $(\mathbb N\cup\{\infty\})^n$ as defining objects and only finitary covers, the computation does come out correctly, as a slightly curious consequence of our new discussion of solid modules.) And I hope you agree that this is a very desirable property. It's the starting point for seeing that the internal notion of group cohomology of all sorts of topological/condensed groups agrees with the various (ad hoc!) notions of continuous group cohomology you can find in the literature.
On the other hand, almost everything we do in condensed sets could also be done already with $\aleph_1$-condensed sets; in fact, I'm contemplating switching to that setting for some things. One nasty issue is that while condensed abelian groups have enough projectives, there are no nontrivial ones that are internally projective. But in $\aleph_1$-condensed abelian groups, $\mathbb Z[\mathbb N\cup\{\infty\}]$ is internally projective!
Regarding 2): As you observe, the theory basically works for any $\kappa$. One thing one might like is that as you increase $\kappa$, the pullback functors are fully faithful. While I don't know whether that's always true, it's true at least when the cardinals are either regular or strong limits. And the reason for choosing strong limits is that in that case, one has enough compact projective objects (the extremally disconnected profinite sets), which are very useful (even if not ultimately necessary) for building the theory.
Regarding 3): The main reason is the desire to avoid artificial choices. Let me elaborate by switching to the next question:
Regarding 4): One thing we prove early on is a general Pontrjagin duality on locally compact abelian groups (even on the derived level). But this requires that there are as many discrete abelian groups as there are compact abelian groups. If you work with $\kappa$-condensed abelian groups, the Pontrjagin duality would force one to restrict not only to $\kappa$-small compact abelian groups, but also to $\kappa$-small discrete abelian groups.
Also, if you really want to say that compactly generated topological spaces embed into condensed sets, without implicitly actually talking about $\kappa$-compactly generated ones, again you need to go this colimit over all $\kappa$.
But in practice, mostly everything is $\aleph_1$-compactly generated, and you can just work with $\aleph_1$-condensed sets (or the much larger category of $\beth_\omega$-condensed sets, where you have enough compact projectives).
But as I said above, you absolutely cannot work with Johnstone's topos, the space $\mathbb N\cup\{\infty\}$ is just too small.