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

  • 1
    $\begingroup$ My (very limited) understanding is that Breen–Deligne defined some sort of "very functorial" resolution, but the usual statement (Thm. 2.1 in the blueprint) does not specify precisely which resolution, making it hard to formalise. Moreover, Commelin e.a. in LTE realised you don't actually need a resolution, just something slightly weaker. The main advantage is that it is now much easier to construct a very hands on example (Def. 2.13), but ultimately the theory does not rely on which example you work with (exactly like how a choice of projective resolution does not matter in the end). $\endgroup$ Commented Feb 6, 2022 at 2:22
  • 1
    $\begingroup$ As to why you would still use the general package, I'm not sure. I can think of two partial answers: (1) it is often easier to work with a conceptual object rather than some explicit (ad hoc) construction, and (2) it is conceivable that different choices of BD package ultimately lead to different constants in Thm. 9.4. $\endgroup$ Commented Feb 6, 2022 at 2:22
  • $\begingroup$ I think it's more that the BD resolution being acyclic is detected by a much more explicit and manageable complex, arising from Mac Lane's work on ring cohomology, being acyclic. Definitely the proof in this section simplifies somewhat, and that was the novelty uncovered in the LTE (mostly by Commelin, but with others pitching in). $\endgroup$
    – David Roberts
    Commented Feb 6, 2022 at 7:11
  • $\begingroup$ Or, rather, the aim is to show that certain Ext groups vanish, and the easier complex is enough to detect this. And the functoriality means that it can be reduced to working with the complex arising from $\mathbb{Z}$ $\endgroup$
    – David Roberts
    Commented Feb 6, 2022 at 7:26
  • 3
    $\begingroup$ The formalization issue with the usual Breen-Deligne resolution isn't that it's not precisely specified (true, but not really a problem), but rather that its existence relies on the finite generation of the stable homotopy groups of spheres, which would be a large amount of additional formalization effort. Otherwise, my understanding agrees with @R.vanDobbendeBruyn's. $\endgroup$ Commented Feb 6, 2022 at 13:28

2 Answers 2


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

  • $\begingroup$ On the relation to $Q'$: if I understand correctly, the MacLane cohomology is equivalent to the topological Hochschild homology. Does your construction give a new insight to that? cf. mathoverflow.net/a/320432 for Bökstedt periodicity for $\mathbb F_p$. $\endgroup$
    – Z. M
    Commented Feb 17, 2022 at 7:19

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.