Ext^i(Mbar(S), V) = 0

Stream: condensed mathematics

[Johan Commelin]

I pushed the statement of $\text{Ext}^i(\bar{ℳ}_{r'}(S), V) ≅ 0$ to src/Mbar/ext.lean. There is a universe mismatch with the version of Thm 9.4 that we proved in liquid.lean.

Explanation: Thm 9.4 is proven by apply Thm 9.5 to the polyhedral lattice $Λ = ℤ$ which lives in Type. This forces S and V to also live in Type. But for universe reasons, we need Thm 9.4 for S and V in Type 1. So we should actually use Λ = ulift ℤ and do a bit more work to show that this is a polyhedral lattice satisfying Hom(ulift ℤ, M) ≅ M.

[Kevin Buzzard]

I'm reading this and it's saying to me "for universe reasons S and V must be more general objects than sets" and the ZFC person in me is going "huh?" This is all because we didn't do the kappa truncation stuff?

[Johan Commelin]

Yes, with κ-truncation we wouldn't have had this problem.

[Johan Commelin]

Anyway, I regard this statement is some sort of watershed.

• To deduce it from (a Type 1-version of) Thm 9.4, we need to prove and use the Breen--Deligne lemma. And then a bit of a diagram chase, taking the limit of the system of complexes in 9.4.
• To go from this statement to the final goal, we need to construct some short exact sequences of condensed abelian groups, and use the resulting long exact sequences for Ext.

[Johan Commelin]

Oooh, and there is a slight catch. What we really need is the ℤ[T⁻¹]-linear version of the statement that I pushed. Instead of the Ab-version.

[Johan Commelin]

I pushed that as a todo comment.

[Adam Topaz]

Hmmm... We can probably leave S : Profinite.{0}, since we want to use Condensed.{0} (Module.{1} ...), right?

[Adam Topaz]

It also depends on how we build our functor from ProFilt...withTinv.{0} to condensed objects.

[Adam Topaz]

I was thinking the functor from ProFilt...{0} would have to land in Condensed.{0} (Module.{1} ...) anyway, since the profinite spaces in the filtration are all in Profinite.{0}.

[Adam Topaz]

Do I understand correctly that the functor condensed in this file Mbar/ext.lean goes from Profinite.{u+1} to Condensed.{u} ??. I don't think this is what we want... It looks like this to_Condensed functor (the last step in the composition defining condensed) might have to be modified? I'm building now so that I can take a closer look at the universes in this file.

The natural functor sends X : ProFilt....{0} to the condensed object which (as a condensed set) is the colimit of X_c.to_Condensed : Condensd.{0} (Type 1) where X_c : Profinite.{0} is the c-th term in the profinite filtration of X, while the well-behaved condensed category in this case would be Condensed.{0} (Module.{1} ??).

[Adam Topaz]

Right, I finished building, and just to confirm, in the line

def condensed : Profinite ⥤ Condensed Ab.{u+1} :=
Mbar.functor.{u+1 u+1} r' ⋙ to_PFPNG₁.{u+1} _ ⋙ to_CHFPNG₁.{u+1} ⋙ to_Condensed.{u}

this is a functor from Profinite.{u+1} to Condensed.{u} Ab.{u+1}. In particular, the last step, to_Condensed.{u} is a functor from CompHausFiltPseuNormGrp₁.{u+1} to Condensed.{u} Ab.{u+1}.

[Adam Topaz]

I think we may have to change this to_Condensed so that it ends up being a functor from CompHausFiltPseuNormGrp₁.{u} to Condensed.{u} Ab.{u+1} (or Condensed.{u} (Module.{u+1} (polynomial (ulift.{u+1} \Z))))

[David Michael Roberts]

Johan Commelin said:

I pushed the statement of $\text{Ext}^i(\bar{ℳ}_{r'}(S), V) ≅ 0$ to src/Mbar/ext.lean. There is a universe mismatch with the version of Thm 9.4 that we proved in liquid.lean.

Explanation: Thm 9.4 is proven by apply Thm 9.5 to the polyhedral lattice $Λ = ℤ$ which lives in Type. This forces S and V to also live in Type. But for universe reasons, we need Thm 9.4 for S and V in Type 1. So we should actually use Λ = ulift ℤ and do a bit more work to show that this is a polyhedral lattice satisfying Hom(ulift ℤ, M) ≅ M.

Just checking that, in the context of Kevin's"ZFC person" comment, the finished part of the proof that made Peter confident (the nasty technical stuff), is 100% free of any of this pyknotic vs condensed issue. I would guess so, and I guess it illustrates how the overarching formalism is really "merely framework", and the real effort is down-to-earth mathematics independent of universes etc.

[Adam Topaz]

I pushed what I'm fairly sure is a fix to the universes into the branch universe-fix. Here is the diff from master
https://github.com/leanprover-community/lean-liquid/compare/universe-fix

[Adam Topaz]

The Ext statement in this branch is now

theorem Ext_iso_zero (S : Profinite.{0}) (V : SemiNormedGroup.{0}) [normed_with_aut r V] (i : ℕ) :
  ((Ext ℤ (Condensed.{0} Ab.{1}) i).obj
    (op $ (condensed.{0} r').obj S)).obj
      (Condensed.of_top_ab V) ≅ 0 :=

[Peter Scholze]

Congratulations on all the progress!

OK, so what's the status now? I was also imagining that Proposition 2.1 of [Analytic] would need to be taken care of? Is anyone (Adam?) working on that?

(This is required for the exact sequence

$0\to \mathbb Z[T^{-1}][S]\to \mathcal M(S,\mathbb Z((T))_r)\to \overline{\mathcal M}_r(S)\to 0$.)

[Johan Commelin]

It's on our radar, but nobody is working on it yet.

[Johan Commelin]

Looking at the proof again, I might have underestimated this... In the MO answer I said that the BD-lemmas was the only big hurdle left. But I guess this is another one.

[Peter Scholze]

Obviously you made really good progress, but actually your post sounded a bit too optimistic to me :-)

[Peter Scholze]

I think there will be at least some struggles coming up...

[Peter Scholze]

For example, you need that the Ext-groups of $\mathbb Z[S]$ against a $p$-Banach $V$, for profinite set $S$, vanish. This should follow from 8.19 that is already formalized, but I think the deduction may need some nonsense on hypercovers that may be a little pain

[Peter Scholze]

Somehow I think while many of the basic definitions are in place, you haven't yet started to do any computation in condensed abelian groups, and I think a few have to be done before you can attack the main one

[Peter Scholze]

Maybe now might be a good time to create some roadmap about what's left to do? I'd be happy to take part in it.

[Adam Topaz]

Does one need hypercovers, or can we get away with a chech nerve associated to $\mathbb{Z}[T] \to \mathbb{Z}[S]$ coming from $T \to S$ a cover with $T$ extr. disc ?

[Peter Scholze]

I think the latter should work too, by some inductive argument.

[Peter Scholze]

(You still need that the complex $\ldots\to \mathbb Z[T\times_S T]\to \mathbb Z[T]\to \mathbb Z[S]\to 0$ is exact, but this is something true in any topos, and in particular before sheafification, where it reduces to the case of sets, and you can write down a contracting homotopy.)

[Peter Scholze]

Or well hmm. I guess I'm certainly using some spectral sequence argument somewhere, implicitly. Not sure what the low effort formalization is.

[Johan Commelin]

I think writing a roadmap is a good suggestion, especially if you offer to help!

[Johan Commelin]

Last time I tried, I ended up writing more lean code instead of a roadmap... :see_no_evil:

[Peter Scholze]

There should probably be a lemma that if you have a presheaf of abelian groups $\mathcal F$ on some site with finite limits and disjoint coproducts that are preserved by $\mathcal F$, and for any cover $T\to S$ the corresponding complex $0\to \mathcal F(S)\to \mathcal F(T)\to \mathcal F(T\times_S T)\to \ldots$ is exact, then $\mathcal F$ is a sheaf with $H^i(S,\mathcal F)=0$ for $i>0$ and all $S$.

[Peter Scholze]

Also, we need $H^i(S,\mathcal F)=\mathrm{Ext}^i(\mathbb Z[S],\mathcal F)$. Maybe this requires the above observation on the complex for $\mathbb Z[S]$'s?

[Johan Commelin]

Wait, do we need sheaf cohomology in a version that is not by definition $\text{Ext}^i(ℤ[S], ℱ)$?

[Peter Scholze]

Hmm OK you might just take that as your definition, but then you need that thing about $\mathbb Z[S]$'s above.

[Peter Scholze]

Or can one deduce the equality directly from the construction as derived functors? You see, I'm a bit lost about the shortest proofs of various "obvious" facts ;-).

[Johan Commelin]

So, if we assumed that S is extr. disc. in the main challenge, then somehow all of this would simplify, right?

[Johan Commelin]

We would still need 2.1, but apart from that, it's only homological algebra, I think

[Peter Scholze]

No this doesn't help, as the relevant $S$'s here are different

[Peter Scholze]

They are some filtration steps in your ProFinFiltBlah's

[Johan Commelin]

Hmm, now I'm confused. If you know that ℤ[S] is projective, then those short exact sequence are enough to deduce the vanishing of $\text{Ext}^i(ℳ_{p'}(S), V)$ for $i > 0$. Or am I missing something?

[Peter Scholze]

You are looking at the easy application of 8.19, there's a more involved application, implicit in this BD stuff

[Johan Commelin]

Aha! Of course. Because we "resolve" by a complex consisting of things like ℤ[ℳ_{≤ c}], and we don't know that those objects are projective!

[Johan Commelin]

I had completely overlooked this issue :see_no_evil:

[Peter Scholze]

Yesterday, I wrote up some quick summary of what's left to do, indicating also how to do some of the diagram chases with Ext-groups etc.; I sent the draft to Johan, who'll probably make it available in some form soon.

I think you're really getting close! I think there's very little foundational stuff that's missing. In particular, one can avoid talking about Ext groups of condensed $\mathbb Z[T^{-1}]$-modules, it can all be said in terms of Ext-groups of condensed abelian groups. About Ext-groups, one only needs to define Ext-groups of complexes of condensed abelian groups (in nonnegative homological degrees) against condensed abelian groups, satisfying a long exact sequence, and sending direct sums to direct products. There was also a question whether one needs tensor products of condensed abelian groups (or even $\mathbb Z[T^{-1}]$-modules): I think not, the only thing one needs are tensor products of condensed abelian groups with (abstract) abelian groups, which are extremely simple to define.

[Johan Commelin]

Here's the document: https://math.commelin.net/files/LTE.pdf . I'll start working on integrating this into the existing blueprint asap.

[Adam Topaz]

One quick comment: Prop 3.3 has also been completely formalized.

[Peter Scholze]

This is great! So as I said above, Adam, I don't think you'll need much more about condensed abelian groups, only the tensor products with abstract abelian groups (and that a tensor product with a free abelian group is the same thing as a (possibly infinite) direct sum of copies of the object).

[Adam Topaz]

What sort of universal property do we need about such an object (the tensor product of a condensed ab with an abstract ab)?

[Peter Scholze]

None, only its construction, and the above property. Well, maybe also that if the condensed abelian group is torsion-free, then this operation is exact in the abelian group.

[Adam Topaz]

Right, I just noticed where it appears in the pdf (middle of page 14)

[Peter Scholze]

In any case, I imagine this should be very straightforward, as you can literally do everything on $S$-valued points, there's no sheafification necessary.

[Adam Topaz]

We'll also need to decide what to do about Ext groups of complexes. Should we just go ahead and define the derived category?

[Peter Scholze]

Hmm, I think you should be able to just barely manage to get through without anything fancy.

[Johan Commelin]

I think what we need most is a projective replacement for bounded-above complexes.

[Peter Scholze]

There's basically only one complex for which you need it, and the relevant triangles arise by truncation. I would imagine that in those cases, the long exact sequence might be formalized directly

[Johan Commelin]

I think we'll also need functoriality of the LES coming from a SES of objects.

[Peter Scholze]

But the specific cases required seem small enough that I don't think it's yet worth the effort to go all the way to derived categories

[Johan Commelin]

Right, but a pretriangulated homotopy category might be helpful.

[Johan Commelin]

To enable the language of triangles, and some abstraction in getting the LES

[Peter Scholze]

I'm not sure it's worth the effort, necessarily... you only need the LES for complexes in a really specific case, for canonical truncations. I would imagine that you can build projective resolutions in such a way that this case becomes very transparent

[Johan Commelin]

Ok, I'll add it to my todo list as one of the things that should be figured out. But we have the pretriangulated unbounded homotopy category already.

[Johan Commelin]

Adding the bounded-above variant shouldn't be too much work, I hope.

[Peter Scholze]

OK, I have no idea on how much work you can already build. It would certainly be more elegant!

[David Michael Roberts]

Adam Topaz said:

What sort of universal property do we need about such an object (the tensor product of a condensed ab with an abstract ab)?

Maybe you don't need it for now, but perhaps it's a copower?

[David Michael Roberts]

@Johan Commelin did you want to add a link to the document in your MO answer?

[Johan Commelin]

Good idea! Done

[Filippo A. E. Nuccio]

I was reading the document, but I don't understand one thing: in the proof of Prop 2.10 to deduce $\mathrm{Ext}^i(K_1,M)=\mathrm{Ext}^{i-1}(K_2,M)=\dots=\mathrm{Ext}^1(K_i,M)$ are you using that $T^{s/n}$ is extremally disconnected? Is this true?

[Filippo A. E. Nuccio]

Ah no, it is just the induction step! Sorry.

[Peter Scholze]

(No, these things aren't extremally disconnected, as I try to explicitly warn at some point. The fragile nature of extremally disconnecteds occupied me for several of the last few months.)

[Filippo A. E. Nuccio]

OK, thanks!