bicomplex glue

Stream: condensed mathematics

[Johan Commelin]

For the glue between the fst part and the snd part, I think we need something like this:

• We have a bicomplex (of abelian groups) $X_{ij}$, with $i,j ∈ ℤ$. Differentials go to the right and downwards.
• If $i \equiv j \equiv 0 \pmod 3$ then $X_{ij} = 0$.
• If $i + j ≤ 0$, then $X_{ij} = 0$.
• If $i \not\equiv 3 \pmod 3$ then $X_{i,•}$ is exact. Analogously for $j$.

Claim: if the remaining columns are exact, then so are the remaining rows.

I couldn't hack together an easy proof using the salamander lemma. What is the correct diagram chase? How should we do this in Lean?

[Johan Commelin]

If it helps at all, the diagram is also (defeq) invariant under $(i,j) ↦ (i+3, j-3)$.

[Peter Scholze]

Johan Commelin said:

For the glue between the fst part and the snd part, I think we need something like this:

• We have a bicomplex (of abelian groups) $X_{ij}$, with $i,j ∈ ℤ$. Differentials go to the right and downwards.
• If $i \equiv j \equiv 0 \pmod 3$ then $X_{ij} = 0$.
• If $i + j ≤ 0$, then $X_{ij} = 0$.
• If $i \not\equiv 3 \pmod 3$ then $X_{i,•}$ is exact. Analogously for $j$.

Claim: if the remaining columns are exact, then so are the remaining rows.

I couldn't hack together an easy proof using the salamander lemma. What is the correct diagram chase? How should we do this in Lean?

Where do we need that?

[Johan Commelin]

Let me try to explain what I have in mind, and then you can tell me if I'm making things more complicated than necessary.
I'll try to write a lot of details, both for myself and for others interested in this step of the proof. The final goal is to show that certain maps between Ext groups are isomorphisms (see below).

We want to get two maps of complexes that form termwise short exact sequences of complexes:

$$\bigoplus_{i : ℕ} Q'(M_{≤ c_i}) ⟶ \bigoplus_{i : ℕ} Q'(M_{≤ c_i}) ⟶ Q'(M)$$

Here:

• the $c_i$ are a suitably chosen increasing sequence of positive real numbers, and we'll get some more constraints on them later
• the first map is "shift minus identity", where "shift" is the map coming from $Q'(M_{≤ c_i}) ⟶ Q'(M_{≤ c_{i+1}})$ (here we using that the sequence is increasing)
• the second map is the natural map coming from all inclusions
• hidden in the notation $Q'(M_{≤ c_i})$ is the choice of extra "Breen-Deligne constants" that are suitable chosen to make sense of the $Q'$-complex

---

Next step: use that $\text{Ext}$ turns coproducts into products (this still needs to be Leanified). So we get a long exact sequence

$$⟶ \text{Ext}^n(Q'(M), V) ⟶ Π_i \text{Ext}^n(Q'(M_{≤ c_i}), V) ⟶ Π_i \text{Ext}^n(Q'(M_{≤ c_i}), V) ⟶ +1$$

For each of these terms we also get "vertical" maps to another copy of this LES (but I don't know how to do diagrams in Zulip):

• $T^⁻¹ - [T⁻¹] \colon \text{Ext}^n(Q'(M), V) ⟶ \text{Ext}^n(Q'(M), V)$
• $T^⁻¹ - [T⁻¹] \colonΠ_i \text{Ext}^n(Q'(M_{≤ c_i}), V) ⟶ Π_i \text{Ext}^n(Q'(M_{≤ c'_i}), V)$ (minor point: in the target we use a sequence of constants $c'_i$ to actually make the maps well-defined: we can take $c'_i = r'c_i$)
• the map is now the map coming from the natural projections
• the second map is now "shift minus identity"

GOAL: show that the map $T^⁻¹ - [T⁻¹] \colon \text{Ext}^n(Q'(M), V) ⟶ \text{Ext}^n(Q'(M), V)$ is an isomorphism.

--

We now use the isomorphisms $\text{Ext}^n(Q'(M_{≤ c_i}), V) ≅ H_n(\hat V(Q'(M_{≤ c_i}))$. This uses the fact that $M_{≤ c_i}$ is a profinite set, so that $Q'(M_{≤ c_i})$ consists of acyclic objects. We also use the isomorphism $\text{Cont}(X, V) ≅ \text{completion of LCC}(X, V) = \hat V(X)$.

So we get LES:

$$⟶ \text{Ext}^n(Q'(M), V) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c_i}))) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c_i}))) ⟶ +1$$

together with the same vertical maps $T^⁻¹ - [T⁻¹]$.

---

We again have two maps of complexes that form termwise short exact sequences:

$$\hat V(Q'(M_{≤ c_i})^{T⁻¹}) ⟶ \hat V(Q'(M_{≤ c_i})) ⟶ \hat V(Q'(M_{≤ c'_i}))$$

• The first map is the inclusion of the kernel of the second map
• The second map is $T^⁻¹ - [T⁻¹]$

So we get LES

$$H_n(\hat V(Q'(M_{≤ c_i})^{T⁻¹})) ⟶ H_n(\hat V(Q'(M_{≤ c_i}))) ⟶ H_n(\hat V(Q'(M_{≤ c'_i}))) ⟶ +1$$

By taking products, we get

$$Π_i H_n(\hat V(Q'(M_{≤ c_i})^{T⁻¹})) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c_i}))) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c'_i}))) ⟶ +1$$

---

Now we can combine these LES in a vertical manner with the "horizontal" LES from above:

$$⟶ \text{Ext}^n(Q'(M), V) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c_i})) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c_i})) ⟶ +1$$

That leaves us with the type of bicomplex that I described in OP.
We have squares

$$Π_i H_n(\hat V(Q'(M_{≤ c_i}))) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c_i})))$$

$$↓\phantom{Π_i H_n(\hat V(Q'(M_{≤ c_i}))) ⟶}↓$$

$$Π_i H_n(\hat V(Q'(M_{≤ c'_i}))) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c'_i})))$$

with vertical maps being $T^⁻¹ - [T⁻¹]$ and the horizontal maps being "shift minus identity".
Above and below these squares, we have horizontal maps

$$Π_i H_n(\hat V(Q'(M_{≤ c_i})^{T⁻¹})) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c_i})^{T⁻¹}))$$

that are again "shift minus identity" (the map below has $H_{n+1}$).

Left and right of the squares we have vertical maps $T^⁻¹ - [T⁻¹] \colon \text{Ext}^n(Q'(M), V) ⟶ \text{Ext}^n(Q'(M), V)$. (The map on the right has $\text{Ext}^{n+1}$.)
Recall that these are the maps that we want to show to be isomorphisms.

---

Final remark: we can show that the horizontal maps above and below the squares are indeed isomorphisms. That's exactly the consequence of first_target aka Thm 9.4. This is where we put a few more conditions on the constants $c_i$.
So we have the "shift minus identity" maps

$$Π_i H_n(\hat V(Q'(M_{≤ c_i})^{T⁻¹})) ⟶ Π_i H_n(\hat V(Q'(M_{≤ c_i})^{T⁻¹}))$$

and we know from Thm 9.4 that the complex $\hat V(Q'(M_{≤ c_i})^{T⁻¹})$ is strongly bounded exact with some constants $k, K$ in degrees $≤ n$ for $c ≥ c₀$.
So we assume that for all $i$ we have

• $c_i ≥ c₀$
• $c_{i+1} ≥ k * c_i$
  and then bounded exactness precisely means that the "shift" map vanishes. So "shift minus identity" is just the identity, hence an isomorphism.
  This final step has been formalized in Lean.

[Johan Commelin]

Ooh, since $c_0$ depends on $n$, I can't even choose the $c_i$ in such a way that they satisfy the constraints for all $n$. So I can't prove that all these maps are isoms in the bicomplex of the OP at the same time. But I can make a choice of constants so that it is true for all $n ≤ N$, for any pre-chosen $N$.

[Peter Scholze]

I think you should reduce the diagrams much earlier! At the point where you have two long exact sequences, with the vertical map $T^{-1}-[T^{-1}]$, you should prove that the following are equivalent (this holds for any map between long exact sequences):

-- every third map is an isomorphism
-- the intermediate squares are bicartesian (i.e. both pullbacks and pushouts; equivalently, give short exact sequences from top left to (direct sum of top right and lower left) to lower right).

Then you only need to prove that certain squares are bicartesian, and all your diagrams are finite.

[Johan Commelin]

Aha, I see. And then we apply this to the two horizontal LES's and then in the other direction to the two vertical LES's.

[Peter Scholze]

Ah, yes

[Johan Commelin]

And we need a version that doesn't use infinite LES's, but only looks at a square squeezed between two isos, or an map squeezed between two bicartesian squares.

[Johan Commelin]

Because of :down:
Johan Commelin said:

Ooh, since $c_0$ depends on $n$, I can't even choose the $c_i$ in such a way that they satisfy the constraints for all $n$. So I can't prove that all these maps are isoms in the bicomplex of the OP at the same time. But I can make a choice of constants so that it is true for all $n ≤ N$, for any pre-chosen $N$.

[Peter Scholze]

Right, but the proof (=diagram chase) clearly only depends on a finite subdiagram

[Johan Commelin]

Yes, but it means we can't cheaply use Cone(f) to prove it.

[Johan Commelin]

So I'll have to think a bit about the most economic way to prove this in Lean.
Unfortunately, these diagram chases are pretty tedious.

[Peter Scholze]

Well, I'll leave those details to you :innocent:

[Johan Commelin]

Maybe there is still a way to use Cone(f). I'll try something out. If so, then we might ditch all the salamander stuff.

[Johan Commelin]

The following is now sorry-free

lemma short_exact [fact (r < 1)] (κ : ℕ → ℝ≥0) [BD.suitable κ]
  [∀ c n, fact (κ₁ c n ≤ r' * (c * κ n))] (c : ℝ≥0ᵒᵖ) (n : ℕ) :
  short_exact ((incl' r r' BD M V κ c).f n) ((Tinv2' r r' BD M V (λ c n, r' * (c * κ n)) (λ c n, c * κ n) c).f n) :=

Translation to ordinary maths: the two maps of complexes

$$\hat V(M_{≤ •}^?)^{T⁻¹} → V(M_{≤ •}^?) → V(M_{≤ r' * •}^?)$$

form termwise short-exact sequences.

[Johan Commelin]

The first map is the "inclusion" and the second map is "$T⁻¹ - [T⁻¹]$".

[Johan Commelin]

The non-trivial bit is the fact that the second map is surjective. This was formalized by @Patrick Massot about a year ago.

The rest is completely trivial on paper: the first object is the kernel of the second map.
But because we didn't set up our definitions in the utmost general way during the first part of the project we now had to do some ugly gluing. But that's done! I was fearing this would be more ugly.

[Johan Commelin]

So now we can get long exact sequences of homology groups of these complexes. We're getting into good shape to show that final Ext groups are vanishing (thanks to the untiring @Adam Topaz who has been hacking on "Ext sends coproducts to products").

[Johan Commelin]

Of course we still need to do the Breen-Deligne lemma. And a little bit of stuff about acyclic complexes.