breen deligne lemma

Stream: condensed mathematics

[Johan Commelin]

I think I've worked out a full proof for the following fact (after some help by Peter :thank_you:). Let $M$ be a condensed abelian group that is torsion free

$$\left(∀ i, \text{Ext}^i(Q'(M), V) = 0\right) \quad \implies \quad \text{Ext}^i(M, V) = 0$$

The proof I have makes use of tensor products of condensed abelian groups, and the fact that the commute with colimits. So we probably want to prove a $⊗ ⊣ \text{Hom}$ adjunction.

[Peter Scholze]

(deleted)

[Johan Commelin]

I'll try to sketch the proof of the above fact in this thread. Recall that $Q'(M)$ is a complex of the form

$$… → ℤ[M^{2^n}] → … → ℤ[M^4] → ℤ[M^2] → ℤ[M]$$

See the Breen--Deligne chapter in the blueprint for the definition of the differential.

[Johan Commelin]

So we get triangles of the form $τ_{≥ i+1} Q'(M) → τ_i Q'(M) → H_i(Q'(M))[i]$.
Note that $τ_0 Q'(M) = Q'(M)$ and $H_0(Q'(M)) = M$.

[Johan Commelin]

Also, $\text{Ext}^i(τ_j Q'(M), V) = 0$ for $i < j$ straightforward from the defn of $τ_j$.

[Johan Commelin]

So now we assume by induction that $\text{Ext}^j(M,V) = 0$ for all $j < i$.

[Johan Commelin]

The $0$-th triangle tells us that $\text{Ext}^i(M,V) = 0$ if we can show that $\text{Ext}^i(\tau_{≥1} Q'(M),V) = 0$.
Now we use the $1$-th triangle, which tells us that we need to prove that $\text{Ext}^i(\tau_{≥2} Q'(M),V) = 0$ and additionally, show that $\text{Ext}^i(H_1(Q'(M))[1], V) = 0$.

[Johan Commelin]

After $i$ such steps, we end up with $\text{Ext}^i(\tau_{≥i} Q'(M),V) = 0$ which is trivially true, and $i$ conditions of the form
$\text{Ext}^i(H_j(Q'(M))[j], V) = 0$.

[Johan Commelin]

Those final conditions follow from the following two claims:

• $H_j(Q'(M)) = H_j(Q'(ℤ)) ⊗ M$
• $\text{Ext}^j(A ⊗ M,V) = 0$ for all object $A$ and all $j < i$ if $\text{Ext}^j(M,V) = 0$ for all $j < i$ (which is our ind.hyp.).

[Johan Commelin]

For the first claim, we write $M$ as a filtered colimit of fin.gen. free objects $ℤ[S]$, where $S$ runs over finite subsets of $M$. (This can be done, because $M$ was assumed torsion free.)
From the definition of $Q'(M)$ we find $Q'(M) = \text{colim}_S Q'(ℤ[S])$. By the homotopy property of $Q'$, we know that it is additive (as functor to the derived category, interesting for Lean!!) and therefore we get $= \text{colim}_S Q'(ℤ)^S$.

[Johan Commelin]

Now we take homology, and use that homology commutes with filtered colimits (because kernels and cokernels do).

[Johan Commelin]

Hence $H_j(Q'(M)) = \text{colim}_S H_j(Q'(ℤ))^S = H_j(Q'(ℤ)) ⊗ M$ as desired.

[Johan Commelin]

Finally, for the second claim above, we take a free resolution $F^•$ of $A$. We can then compute

$$\text{Ext}^j(A ⊗ M, V) = H_j(\text{Hom}(F^• ⊗ M, V))$$

and since the $F^k$ are free, we can pull them out of the tensor and the hom, and turn the direct sums into products. The result vanishes by the ind.hyp.

[Johan Commelin]

As a final remark. If $M$ comes equipped with a distinguished endomorphism (so that it is a condensed $ℤ[T⁻¹]$-module), then all the above is $T⁻¹$-equivariant, and all the computations still make sense. So the lemma in the first post also holds for Ext groups of $ℤ[T⁻¹]$-modules (which is what we need).

[Johan Commelin]

I think we can avoid defining the derived category (which is probably a pain if we don't want to bump universes and still be general). We can exhibit a quasi-isomorphism between $Q'(A ⊕ B)$ and $Q'(A) ⊕ Q'(B)$. It should be possible to work with that. Although it will make the proof a bit uglier.

[Riccardo Brasca]

Wow, that's amazing!

[Kevin Buzzard]

This is the sort of mathematics which I had somehow imagined would be "trivial to formalise in a theorem prover, and probably done many times already by Voevodsky and others", before I knew anything about theorem provers.

[Kevin Buzzard]

Everything follows from the axioms so it must all be trivial, right?

[Kevin Buzzard]

Someone once said to me that Lean makes doing maths in a theorem prover about as easy as you thought doing maths in a theorem prover would be before you actually tried to use a theorem prover.

[Johan Commelin]

Well, I'm a bit scared by that tensor product. One thing that will help a lot is if we can check things on extremally disconnecteds. For example, there you don't need to sheafify the tensor product.

[Johan Commelin]

We finally have a formal statement of the BD lemma:

lemma main_lemma (A : 𝒜ᵒᵖ) (B : 𝒜) (f : A ⟶ A) (g : B ⟶ B) :
  (∀ i, is_iso $ ((Ext' i).map f).app B - ((Ext' i).obj A).map g) ↔
  (∀ i, is_iso $
    ((Ext i).map ((BD.eval F).op.map f)).app ((single _ 0).obj B) -
    ((Ext i).obj ((BD.eval F).op.obj A)).map ((single _ 0).map g)) :=

Blueprint: https://leanprover-community.github.io/liquid/sect0009.html#Qprime-prop

[Johan Commelin]

Reading this statement makes me wonder whether we should have actually tried to work with ℤ[T⁻¹]-modules. But I think it's fine.

[Johan Commelin]

The administration of working with

is_iso $
    ((Ext i).map ((BD.eval F).op.map f)).app ((single _ 0).obj B) -
    ((Ext i).obj ((BD.eval F).op.obj A)).map ((single _ 0).map g))

aka

$$f^* - g_* \colon \text{Ext}^i(Q'(A), B) \to \text{Ext}^i(Q'(A), B) \qquad \text{is an iso}$$

for maps $f \colon A \to A$ and $g \colon B \to B$ didn't look very appetizing. So I decided to bundle everything up into the category of endomorphisms, with objects $(A,f)$.
If $A$ was an object of $\text{Ab}$, then the resulting category is of course equivalent to $\mathbb{Z}[X]\text{-Mod}$.

The upshot is that (modulo a few sorrys) we now only need to work with

is_zero (((Ext i).obj A').obj B')

where A' and B' are now objects of an arbitrary ab.cat (potentially this category of endomorphisms).

[Johan Commelin]

There is plenty of low-hanging fruit in for_mathlib/endomorphisms/*.

[Kevin Buzzard]

I will have time this evening (but probably not before).

[Kevin Buzzard]

I took a look at the files on the tube to work (where I can't mark!). This claim map_homotopy_category_is_bounded_above in endomorphisms.Ext says that if a complex is bounded below and you hit it with an additive functor it remains bounded below. I am confused about this. Is the functor Ab -> Ab sending all abelian groups to $\mathbb{Z}/37\mathbb{Z}$ and all morphisms to the zero morphism, additive? If so then it sends bounded below complexes to not-bounded-below complexes. Where did I screw up?

[Johan Commelin]

Hmm, you can't send identity maps to 0, right?

[Johan Commelin]

additive functors preserve zero homs, and hence zero objects. Because you are a zero object iff id = 0.

[Adam Topaz]

Do we have something liike functor.map_is_zero for an additive functor? I suppose not.

[Adam Topaz]

Ah we have docs#category_theory.functor.map_zero_object

[Kevin Buzzard]

OK I removed the sorry.

[Kevin Buzzard]

I also added functor.map_is_zero (to this endomorphism file :-/ Where does it go?)

[Adam Topaz]

@Kevin Buzzard I moved your lemma to for_mathlib.additive_functor

[Johan Commelin]

• The Breen-Deligne lemma (for arbitrary abelian cats having a tensor product with a suitable property) is sorry free.
• The check that Condensed Ab satisfies the property is also sorry free.

Major kudos to @Joël Riou and @Kevin Buzzard for working on this stuff!