overview of what's left

Stream: condensed mathematics

[Johan Commelin]

I think it might be useful to have an overview of what's left to be done.

• Kevin and Filippo are working on stuff related to the quotient $\mathbb Z((T))_{r'} \to \mathbb R$. Proving continuity seems to require quite an effort, but there's a clear plan of attack and so I expect this is just a matter of time.
• There was a small hiccup related to invpoly. I know how to fix this, and I think I'll work on that tomorrow.
• There's a whole slew of sorrys related to homological algebra. These just need to be done, but I think that should be pretty straightforward.
• To prove the BD lemma, we need to use all that homological algebra. I'll write a more detailed list of things needed for that.
• Finally we need to glue first_target into Ext_Lbar. One puzzle piece that we need for this:
  • Ext(_, V) sends infinite direct sums to infinite products.

[Filippo A. E. Nuccio]

(deleted)

[Johan Commelin]

For the BD lemma, here's a more detailed list

• the truncation functors $\tau_n$
• the complex $\text{imkerseq}_n C$ (I just made up this name) which is $\ker(d)$ in degree $n$ and $\text{im}(d)$ in degree $n+1$
• the homology of $\text{imkerseq}_n C$, which is just $H_n(C)$ in degree $n$ and 0 elsewhere
• reformulate this homology computation as a quasi-isomorphism
• the natural map $\tau_{n+1}C \to \tau_n C$
• the natural map $\tau_n C \to \text{imkerseq}_n C$
• the proof that these two maps form termwise short exact sequences

[Johan Commelin]

Finally, we also need a bit about tensor products of condensed abelian groups with (discrete) abelian groups.

[Filippo A. E. Nuccio]

I hope to finish this continuity business soon (hopefully in the week-end?) and then I might attack something else.

[Johan Commelin]

It will be really nice to see that part finished! Happy for you!

[Filippo A. E. Nuccio]

OK, as promised most of the continuity stuff has been done. The file ses.lean went down to 2 sorries. I still have a troublesome (deterministic) timeout in the proof of lemma U_subset_preimage: there is a calc block that causes the lemma to timeout: @Johan Commelin can you have a look, at a certain point?

[Filippo A. E. Nuccio]

I will move on and to the profinite topological lemma is_open_U starting tomorrow.

[Filippo A. E. Nuccio]

(deleted)

[Adam Topaz]

Filippo A. E. Nuccio said:

I will move on and to the profinite topological lemma is_open_U starting tomorrow.

Where is this lemma? I might have time to take a look this afternoon (assuming I finish marking some final exams)

[Johan Commelin]

Wow, down to 2 sorries. That's progress! I'm still sitting in a massively delayed train with a 20kb/s internet connection. So zulip is the only thing that works, and I can't get the oleans that I need.

[Johan Commelin]

But I should have time to look at this tomorrow, if it's not solved by then.

[Riccardo Brasca]

I will have time to help starting on Sunday. Let me know if there is something I can do.

[Johan Commelin]

Thanks! That's very helpful. Would you prefer diagram chases? Or do you want to put your teeth in the Breen-Deligne lemma?

[Johan Commelin]

(@Kevin Buzzard I moved your message to this thread.)

[Johan Commelin]

I think naturality of the snake delta is also a really nasty remaining bit. Because we constructed that delta using a bundled version of the snake lemma. That was nice for proving the snake lemma. But it was completely unusable. So then I reproved the snake lemma in unbundled form, by reducing it to the bundled version. However, this transition involved ugly DTT glue, even though it's math-content free. It's not clear to me what this means for the delta.

[Riccardo Brasca]

I can try naturality. There no homotopy/triangulated catgories involved, right? (I am not familiar at all with that part of the library)

[Johan Commelin]

Sure, it's just hands-on diagram chasing in abelian categories, no triangulated stuff. But it might be good to map out the exact problem before writing pages of code.

[Adam Topaz]

I just added a file called for_mathlib/snake_lemma_naturality with a few small sorries remaining for the naturality of the snake lemma.
These sorries should all be fairly easy

[Johan Commelin]

is_snake_input.to_kernel._proof_2 ugh... :see_no_evil:

[Adam Topaz]

I just copied/pasted. Feel free to clean up!

[Riccardo Brasca]

Thanks! I will have a look in 48 hours if nobody beats me

[Johan Commelin]

I put the notation

local notation x `⟶[`D`]` y := D.map (snake_diagram.hom x y)

back in place. So now those _proof_2 are gone.

[Adam Topaz]

Great! Can you push?

[Adam Topaz]

Nevermind... got it!

[Johan Commelin]

Thanks a lot for doing this. But one sobering warning: constructing that $\eta$ which is a map between snake diagrams is going to be pretty painful. We'll need to fight DTT and "large" finite categories there.

[Johan Commelin]

"large" in the sense that there are 12 objects and 17 morphisms. So there's a lot to write down when building such an eta, and even more to check.

[Johan Commelin]

Here's what I did for constructing that diagrams aka functors: https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/fin_functor.lean

[Adam Topaz]

We just need a constructor for such an $\eta$ given a bunch of commuting squares.

[Adam Topaz]

Okay, I finished off the sorries in snake_lemma_naturality.

[Adam Topaz]

I guess we'll need some more (smallish) glue to get a version that's unbundled (similar to what @Johan Commelin mentioned above)

[Adam Topaz]

And we'll need to figure out how to construct such $\eta$.

[Johan Commelin]

Constructing such an eta from unbundled information is what's needed.

[Adam Topaz]

Do you have an example of such "unbundled information" that's used in practice?

[Johan Commelin]

Would that also solve the snake delta sorry in derived/les2.lean?

[Adam Topaz]

Well, I think we would need the $\eta$-constructor for that les2 sorry

[Adam Topaz]

Since the $\eta$ includes maps between the kernels/cokernels that exist just because they are kernels and cokernels

[Johan Commelin]

We also need it here: https://github.com/leanprover-community/lean-liquid/blob/master/src/Lbar/squares.lean#L85

[Adam Topaz]

Ah okay, so we could really use a constructor for $\eta$ given a commuting square of short exact sequences :)

[Johan Commelin]

But that les2 sorry is saying that a certain map that isn't delta on the nose is still equal to delta. Does that follow from the naturality of delta? Or is it just another computation?

[Johan Commelin]

Another todo that should be easy to jump into without context is

• bicartesian_of_id_of_end_of_end_of_id

It's another one of those diagram chases.

[Johan Commelin]

I will try to state the unbundled version of delta naturality later today. I'll be interested to know if it closes the les2 sorry.

[Adam Topaz]

I think that les2 sorry wouldn't follow immediately, but I hope that naturality of $\delta$ will simplify the calculation significantly.

[Johan Commelin]

For all that are happy to join the forces of pushing LTE across the finish line: I'll try to extract a bunch of sorries into small files that can hopefully be attacked in a pretty context free manner.

[Johan Commelin]

Search for -- SELFCONTAINED to find these sorries.

[Johan Commelin]

I just pushed 3 new files with such sorries. More should follow soon.

[Yaël Dillies]

291 commits to pull, you guys are crazy!

[Johan Commelin]

That doesn't mean anything if you don't tell when you last pulled :wink:

[Yaël Dillies]

It was a week ago I believe.

[Adam Topaz]

I added two more STANDALONEs in for_mathlib/snake_lemma. These are just playing with pseudoelements.

[Adam Topaz]

And the conclusion is the universal property of $\delta$:

lemma eq_δ_of_spec (e : D.obj (0,2) ⟶ D.obj (3,0))
  (he : hD.to_kernel' ≫ e ≫ hD.cokernel_to' = kernel.ι _ ≫
    D.map (hom (1,1) (2,1)) ≫ cokernel.π _) :
  e = hD.δ := ...

@Kevin Buzzard you might be interested in this!

[Kevin Buzzard]

I have two talks in the next three days and also 300 analysis scripts to mark, I might have to take a few days off Lean :-(

[Johan Commelin]

Adam Topaz said:

I added two more STANDALONEs in for_mathlib/snake_lemma. These are just playing with pseudoelements.

Thanks! I changed them to SELFCONTAINED. For consistency :wink:

[Adam Topaz]

Oops!

[Riccardo Brasca]

I've done exact_factor_thru_image_iff. I hope nobody is against pseudoelements :)

[Riccardo Brasca]

Also iso_of_short_exact_comp_right is done.

[Riccardo Brasca]

exact_iff_image_to_kernel'_is_iso and homology_is_zero_iff_image_to_kernel'_is_iso are done.

[Johan Commelin]

Nice progress!

[Adam Topaz]

The proof that (cone.\pi f) is a quasi-iso is now sorry-free in for_mathlib/derived/les2. This file now has a LOT of non-terminal simps and very slow proofs. If you like to golf, please take a look!

[Riccardo Brasca]

I was having a look at bicartesian_of_id_of_end_of_end_of_id, but I am confused. How are we supposed to prove that is_iso (kernel.map g g β γ _)? We have docs#category_theory.limits.kernel.map_iso, but this of course requires the vertical maps to be isos, and I don't see why the other conditions in bicartesian_of_id_of_end_of_end_of_id should force β to be an iso.

[Riccardo Brasca]

The four/five lemma doesn't seem to apply.

[Markus Himmel]

I pushed a proof. The trick was finding the correct diagram to apply the five lemma to.

[Riccardo Brasca]

Nice, thanks!

[Johan Commelin]

Thanks for doing these!

[Johan Commelin]

There's 3 SELFCONTAINED left now (-;

[Johan Commelin]

I'll try to make some more

[Johan Commelin]

I've been attacking derived/les2.lean. It's starting to get into good shape

[Johan Commelin]

It's sorry-free. Some of these sorries were pretty old. I'm really glad that they are gone.
Along the way, the file was split into les2.lean and les3.lean.

[Adam Topaz]

To to summarize, I think we now have sorry-free essentially everything we need in terms of the long exact sequences! Is that right?

[Johan Commelin]

There's one sorry left in les_facts.lean

[Johan Commelin]

Once that one is done, we can close two more ovals. (Unless I missed something...)

[Johan Commelin]

I'm now extracting that sorry into something self-contained. It is once again a δ-naturality thing.

[Johan Commelin]

Hmm, it's a bit of an annoying one. I guess it goes all the way back to how we constructed the LES for maps of complexes that are termwise short exact, using cones, and all that.

[Johan Commelin]

I pushed what I have. The sorry has moved back to les2.lean...

[Adam Topaz]

@Johan Commelin I don't see any sorries in les2.

[Johan Commelin]

Aah snap, I meant les3.

[Johan Commelin]

@Riccardo Brasca Is this one for you?

-- src/for_mathlib/derived/Ext_lemmas.lean
def Ext'_zero_flip_iso (B : A) :
  (Ext' 0).flip.obj B ≅ (preadditive_yoneda.obj B) :=
sorry

[Adam Topaz]

Do we have the functoriality of cone somewhere?

[Peter Scholze]

This sounds like a dangerous question... (the cone famously not being functorial in the homotopy category or derived category)

[Adam Topaz]

In this case we just have concrete cochain complexes, so I think it should be okay

[Johan Commelin]

Yes, in that case it should be done.

[Johan Commelin]

See https://github.com/leanprover-community/lean-liquid/blob/287eb043aed4eff93d738ae4b22442ace9ce1882/src/for_mathlib/mapping_cone.lean#L139-L161

[Johan Commelin]

(cc @Adam Topaz)

[Adam Topaz]

Thanks!

[Adam Topaz]

Okay, I'm about to push a proof of Ext_δ_natural, but I should apologize ahead of time for another block of excruciatingly slow proofs....

[Riccardo Brasca]

Johan Commelin said:

Riccardo Brasca Is this one for you?

-- src/for_mathlib/derived/Ext_lemmas.lean
def Ext'_zero_flip_iso (B : A) :
  (Ext' 0).flip.obj B ≅ (preadditive_yoneda.obj B) :=
sorry

I can have a look.

[Riccardo Brasca]

Hmm, to be honest I am not very familiar with Ext'. What we have is docs#category_theory.abelian.functor.left_derived_zero_iso_self (and also the dual version for right derived functors), but I don't know how to connect Ext' with a mathlib-style derived functor. Is this somewhere?

[Adam Topaz]

@Riccardo Brasca this iso should be relatively straightforward by using bounded_homotopy_category.hom_single_iso from for_mathlib/derived/example.

[Adam Topaz]

Ext m A B is defined as Hom(A',B[m]) where A' is a K-projective replacement of A. Now B[0] is iso to B (see shift_zero) and the iso I mentioned in my last message tells you that this can be computed using homology. Now you should be able to use the "replacement" part in the K-projective replacement to get the required iso.

[Adam Topaz]

Well, maybe it would be easier to just use Ext'_iso:
https://github.com/leanprover-community/lean-liquid/blob/50916763100554eda136d132a3e5be342d3a3da9/src/for_mathlib/derived/example.lean#L444

That reduces the computation to the "classical" version of Ext.

[Riccardo Brasca]

I am not saying it's hard, just that there is surely someone that can do a better job that myself :sweat_smile:

[Johan Commelin]

Adam Topaz said:

Okay, I'm about to push a proof of Ext_δ_natural, but I should apologize ahead of time for another block of excruciatingly slow proofs....

Cool! That turned out to be easier than I feared.

[Johan Commelin]

I'm going to make Ext-L and main-thm green. They still depend on sorrys of course, but only on sorrys represented by other ovals in the graph.

[Adam Topaz]

I added a skeleton for Ext'_zero_flip_iso. Most of the sorries are self-contained, and are located in for_mathlib/derived/ProjectiveResolution.

[Adam Topaz]

There is one sorry in Ext_lemmas about naturality as well.

[Adam Topaz]

The sorries in for_mathlib/derived/ProjectiveResolution are all done, but the naturality sorry in Ext_lemmas still remains (with some progress).

[Adam Topaz]

I decided to take a different approach, but, overall,

def Ext'_zero_flip_iso (B : A) :
  (Ext' 0).flip.obj B ≅ (preadditive_yoneda.obj B) :=

is sorry free

[Johan Commelin]

Nice. I need to give a talk today, and the preparations are taking some time. I hope to be back in action asap.

[Johan Commelin]

I pushed two new self-contained sorries to src/for_mathlib/exact_lift_desc.lean. They set up an API for exact.lift and exact.desc.

[Johan Commelin]

Ooh, that conflicts with docs#category_theory.exact.lift so I've renamed stuff in the new file to mono_lift for now.

[Markus Himmel]

I filled the sorries, but please note that the results of exact_lift_desc.lean are all in mathlib already, as docs#category_theory.abelian.is_limit_of_exact_of_mono and docs#category_theory.abelian.is_colimit_of_exact_of_epi.

[Johan Commelin]

Ok, thanks!

[Johan Commelin]

Still, I think these are useful wrapper, if only because of dot-notation. Do you agree?

[Markus Himmel]

Yes, I think it's fine in this case. But maybe we should redefine exact.mono_lift in terms of is_limit_of_exact_of_mono so that it's easy to add things that we already know for kernels (like hom_ext) as needed.

[Johan Commelin]

Sounds good. Feel free to do so

[Johan Commelin]

There is now

-- SELFCONTAINED
lemma homology_map_homology_op_iso {A₁ B₁ C₁ A₂ B₂ C₂ : 𝓐}
  (f₁ : A₁ ⟶ B₁) (g₁ : B₁ ⟶ C₁) (w₁ : f₁ ≫ g₁ = 0)
  (f₂ : A₂ ⟶ B₂) (g₂ : B₂ ⟶ C₂) (w₂ : f₂ ≫ g₂ = 0)
  (a : A₁ ⟶ A₂) (b : B₁ ⟶ B₂) (c : C₁ ⟶ C₂)
  (sq1 : commsq f₁ a b f₂) (sq2 : commsq g₁ b c g₂) :
  homology.map' _ _ sq2.op sq1.op ≫ (homology_op_iso f₁ g₁ w₁).hom =
  (homology_op_iso _ _ _).hom ≫ (homology.map' w₁ w₂ sq1 sq2).op :=
begin
  delta homology_op_iso, dsimp,
  sorry
end

in for_mathlib/is_quasi_iso.lean.
It's the final remaining sorry that is left to show that Ext can be computed using acyclic resolutions.

[Adam Topaz]

I've got a proof of this.

[Adam Topaz]

Pushing in a few minutes...

[Adam Topaz]

For future reference, whenever possible please PLEASE try to use docs#homology.desc' and docs#homology.lift to construct maps in/out of homology.

[Adam Topaz]

I think we should (eventually) redefine homology similarly to how biproducts are defined in mathhlib as some gadget which is both a kernel and a cokernel.

[Johan Commelin]

Number of files with sorrys is going down fast!

1 src/breen_deligne/main.lean
5 src/condensed/acyclic.lean
1 src/for_mathlib/acyclic.lean
11 src/Lbar/ext.lean
2 src/pseudo_normed_group/QprimeFP.lean
20 total

[Johan Commelin]

There are 2 SELFCONTAINED sorries in condensed/acyclic.
One is the fact that being projective is isomorphism-invariant, the other is a diagram chase.

[Markus Himmel]

I will do both of them today

[Markus Himmel]

I did the chase. Isomorphism invariance of projectivity is already in mathlib, so I deleted it.

[Kevin Buzzard]

What's the mathematical summary of what's left?

[Johan Commelin]

@Markus Himmel Thanks!

Mathematical summary of what is left:

• The first paragraph of https://leanprover-community.github.io/liquid/sect0009.html#acyclic-sheaf (exactness of that complex).
• The Breen-Deligne lemma

Summary of non-mathematics that is left:

• Glue with the first part.

[Johan Commelin]

See https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/overview.20of.20what's.20left/near/280485297 upstream for a todo list on BD.

[Adam Topaz]

I can probably take care of the first item next week.

[Kevin Buzzard]

What is "the Breen-Deligne lemma"?

[Johan Commelin]

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

[Johan Commelin]

Johan Commelin said:

For the BD lemma, here's a more detailed list

• the truncation functors $\tau_n$
• the complex $\text{imkerseq}_n C$ (I just made up this name) which is $\ker(d)$ in degree $n$ and $\text{im}(d)$ in degree $n+1$
• the homology of $\text{imkerseq}_n C$, which is just $H_n(C)$ in degree $n$ and 0 elsewhere
• reformulate this homology computation as a quasi-isomorphism
• the natural map $\tau_{n+1}C \to \tau_n C$
• the natural map $\tau_n C \to \text{imkerseq}_n C$
• the proof that these two maps form termwise short exact sequences

I pushed a skeleton with these statements to for_mathlib/truncation.lean. No condensed maths involved, just some complexes. There is sorried data, but it should all be pretty self-contained.

[Kevin Buzzard]

I am not reading properly because I'm doing what I'm supposed to be doing, but I don't understand the definition of imkerseq_n(C). The map from ker(d) to im(d) is the zero map, right? So there will be homology in degree n+1 right?

[Johan Commelin]

This was written with chain complexes in mind, so the maps go the other way.

[Johan Commelin]

The only interesting differential should be the inclusion im(d) → ker(d).

[Kevin Buzzard]

/-- The natural map from `H_n(C)[n]` to `imker C n`. -/
def from_single (n : ℤ) : (single _ _ n).obj (C.homology n) ⟶ C.imker n :=
sorry

This sorried data looks suspicious to me -- shouldn't the map be the other way round @Johan Commelin ?

[Johan Commelin]

@Kevin Buzzard Oops, of course!

[Johan Commelin]

That's the whole point... that we can't have a triangle between truncations and homology in the homotopy category because we need to invert this quasi iso first.

[Johan Commelin]

I blind-pushed an attempt to fix it. I hope it builds. I can't build on my current device.

[Adam Topaz]

I think this change broke breen_deligne/main by breakiing for_mathlib/truncation_Ext. I'll try to fix this later today if I have time.

[Adam Topaz]

Okay, I think it should be fixed now.

[Johan Commelin]

It seemed to build fine locally when I tried to fix things, but it must have been a fluke.

[Johan Commelin]

Thanks for fixing!