I am trying to understand some things about Condensed Mathematics and the Liquid Tensor Experiment. The aim of the LTE is to provide a formalised proof of Theorem 9.4 in Scholze's paper Lectures on Analytic Geometry (describing joint work with Clausen). Part of the LTE is a blueprint of the general approach. Theorem 9.4 is stated for a rather general class of chain complexes, but the blueprint works with a more restricted class which is presumably sufficient for the intended application; I have not yet understood this reduction. Specifically, the blueprint considers complexes defined with the aid of a structure called a Breen-Deligne package (Definition 2.11 in the blueprint). As pointed out in Definition 2.13 of the blueprint, there is a default example of a Breen-Deligne package. My question is: is it sufficient to consider this default example, or is there a real need to consider all possible examples?
If it is sufficient to consider the default example, then it seems to me that the whole proof can be substantially simplified. (However, I am just beginning to get to grips with these ideas, so I could easily be mistaken.)
Best Answer
The comments have already given the answers, but let me assemble them here with my account of the story.
When Scholze first posted the Liquid Tensor Experiment, it was quickly identified (by both Peter and Reid, somewhat independently I think) that Breen–Deligne resolutions would be the largest input in terms of prerequisites that needed to be formalised. Back then, I had no idea what these resolutions were, or how to prove that they existed. But they were needed for the statement of Theorem 9.4, which seemed to be a very natural first milestone to aim for.
So I set out to formalise the statement of the existence of Breen–Deligne resolutions, with the expectation that we would never prove the result in Lean, but just assume it as a black box. Let me recalll the statement:
Theorem (Breen–Deligne). For an abelian group $A$, there exists a resolution of the form $$ \dots → \bigoplus_{j = 0}^{n_i} ℤ[A^{r_{i,j}}] → \dots → ℤ[A^2] → ℤ[A] → A → 0 $$ that is functorial in $A$.
On the proof. See appendix to Section IV of Condensed.pdf. As Reid remarked in the comments, the proof relies on the fact that stable homotopy groups of spheres are finitely generated. ∎
(Aside: for the proof of Theorem 9.4, we really need a version that applies to condensed abelian groups $A$, so in practice we want to abstract to abelian sheaves.)
In the rest of the Lecture notes, Scholze often uses a somewhat different form of the above resolution, by assuming $n_i = 1$ and effectively dropping all the $\bigoplus$'s. I think this was done mostly for presentational reasons.
I did the same thing when I axiomatized Breen–Deligne resolutions in Lean. So really, they weren't axiomatized at all. I don't know of any reason to expect that there exists a resolution with the property that $n_i = 1$ for all $i$, but I also don't see any reason why there shouldn't. Anyway, I needed a name for the axioms that I did put into Lean, and I chose Breen–Deligne package for that.
So what is that exactly? Well, a functorial map $ℤ[A^m] → ℤ[A^n]$ is just a formal sum of matrices with coefficients in $ℤ$. So as a first approximation, we record
But we need one more property of Breen–Deligne resolutions: if $C(A)$ denotes the complex, then there are two maps induced by addition. There is the map $σ \colon C(A^2) → C(A)$ that comes from the functoriality of $C$ applied to the addition map $A^2 → A$. But there is also the map $π \colon C(A^2) → C(A)$ that comes from addition in the objects of the complex. (All objects are of the form $ℤ[A^k]$ and we can simply add elements of these free abelian groups.) The final axiom of a Breen–Deligne package is
While playing around with the axioms, I noticed that I could write down inductively a somewhat non-trivial example of such a package. When I discussed this example with Peter, he suggested that it might in fact be suitable as a replacement for Breen–Deligne resolutions in all applications in his lecture notes so far. Several months later we found out that I had rediscovered MacLane's $Q'$-construction. So, let's denote by $Q'$ the complex corresponding to the example package. The following result is, as far as I know, original:
Lemma. Let $A$ and $B$ be (condensed) abelian groups. If $\text{Ext}^i(Q'(A),B) = 0$ for all $i ≥ 0$, then $\text{Ext}^i(A,B) = 0$ for all $i ≥ 0$.
Proof. I've written up a proof sketch on Zulip (public archive of that thread). ∎
We are in the process of formalizing the necessary homological algebra to verify the proof in Lean. It's the last major milestone left to complete the challenge in Peter's original blogpost. After that, we mostly need some glue. See this blogpost for an update on the formalisation effort. (Edit: see also https://math.commelin.net/files/LTE.pdf for a more precise roadmap of what remains to be done to complete the challange.) Once everything is done, it should all be written up in some paper.
So now, let me turn to the question
It is indeed sufficient to consider this default example. The reasons for working with the abstract concept of Breen–Deligne packages are
What would be really interesting is an example of a BD package that gives resolutions instead of merely functorial complexes. It is known that the $Q'$ construction is not a resolution. Indeed, one can easily show inductively that $H_i(Q'(ℤ))$ contains a copy of $ℤ^{2^i}$. With more work (relying again on abstract homotopy theory), Peter gave a proof that $Q'(A) ≅ Q'(A)^{⊕2}[-1] ⊕ ℤ ⊗_{\mathbb S} A$ on Zulip (public archive).