Breen-Deligne packages and the liquid tensor experiment

Question

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.)

Answer 1

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

• the natural numbers $r_j = r_{1,j}$ (since $n_i = 1$);
• for every $j$, a formal sum of $(r_{j+1}, r_j)$-matrices with coefficients in $ℤ$.

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

• there is a functorial homotopy between $σ$ and $π$.

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

is it sufficient to consider this default example, or is there a real need to consider all possible examples?

It is indeed sufficient to consider this default example. The reasons for working with the abstract concept of Breen–Deligne packages are

• historical: I had formalised the statement of Theorem 9.4 and some other material in terms of BD packages before I realised that this default example was indeed sufficient for our purposes.
• practical: as Remy points out in the comments, it is (i) helpful to abstract away concrete details into a conceptual object, and (ii) there is a chance that there might be better examples leading to better constants.

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).

Answer 2

This is not an answer about Breen–Deligne packages, but a long remark on Breen–Deligne resolution(s) per se.

Notation. Let $\DeclareMathOperator\Ab{Ab}\DeclareMathOperator\free{free}\DeclareMathOperator\fg{fg}\Ab$ denote the category of abelian groups, $\Ab^{\free,\fg}$ the category of free abelian groups of finite rank. More generally, let $R$ be a ring, we denote by $\DeclareMathOperator\Proj{Proj}\Proj^{\fg}(R)$ the category of finitely generated projective $R$-modules. Note that $\Ab^{\free,\fg}=\Proj^{\fg}(\mathbb Z)$.

As shown in [Lecture on Condensed Mathematics, Thm 4.14], we can rephrase the existence of Breen–Deligne resolution as:

Theorem. The functor $\Ab^{\free,\fg}\to\Ab,P\mapsto P$ is pseudocoherent in the abelian category $\DeclareMathOperator\Fun{Fun}\Fun(\Ab^{\free,\fg},\Ab)$.

Some mentioned that a crucial difficulty is that its usual proof relies on some input from stable homotopy theory which is not currently formalized in computer proof assistant systems. I want to point out that there is a recent proof, if I understand correctly, without obvious reference to stable homotopy theory, but rather via functor homology. More precisely, it is the following:

Theorem. ([Djament–Touzé, Thm 2]) Let $A$ be a finitely generated $\mathbb Z$-algebra, $k$ a Noetherian ring, and $\DeclareMathOperator\Mod{Mod}F: \Proj^{\fg}(R)\to\Mod_k$ a polynomial functor. If $F$ is finitely generated (aka. 0-pseudocoherent) in the abelian category $\Fun(\Proj^{\fg}(R),\Mod_k)$, then it is a Noetherian object there.

In particular, when $R=k=\mathbb Z$, and $F$ is the canonical inclusion, we deduce the existence of Breen–Deligne resolution.

A note on history: this type of result was first obtained by Schwartz in Franjou–Lannes–Schwartz to deduce the Bökstedt periodicity of the MacLane cohomology (equivalently, the topological Hochschild cohomology) for finite fields.