condensed/exact.lean

Stream: condensed mathematics

[Scott Morrison]

In condensed/exact.lean, Johan was attempting to construct some isomorphisms which should just come from the fact that limits commute. I've done this (at least for P1, not yet P2) on a branch condensed_exact. It needs #13215 merged into mathlib, and lean-liquid bumped, before that branch can be merged with master.

[Scott Morrison]

(If someone could merge #13215 when it's ready, that would be great. It's hopefully noncontroversial.)

[Scott Morrison]

(Also #13216 which contains the other mathlib-appropriate part of this branch.)

[Adam Topaz]

I left a comment on #13215

[Johan Commelin]

We'll have to brace ourselves for the mathlib bump. But it needs to be done at some point. So let's get it over with.

[Johan Commelin]

I'm starting a bump

[Riccardo Brasca]

If you want some help I can work on it, but it's probably not very easy to coordinate the work.

[Johan Commelin]

@Riccardo Brasca If you want to take on that pseudo-element proof, that would be cool!

[Johan Commelin]

I mean this one: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/pseudoelements/near/278122957

[Johan Commelin]

I guess the bump will indeed be hard to parallelize

[Riccardo Brasca]

Okay, I will work on the proof

[Riccardo Brasca]

Do you mean the last sorry, right? Not have aux : ∀ n, short_exact ((kernel.ι π).f n) (π.f n) .

[Johan Commelin]

Sure that one should be trivial.

[Johan Commelin]

We just need a lemma that says proves short_exact (kernel.\iota f) f given epi f

[Johan Commelin]

But the last one is trickier, I fear.

[Riccardo Brasca]

Yes, the first one is docs#category_theory.exact_kernel_ι

[Johan Commelin]

Plus mono (kernel.\iota f) which should be infer_isntance

[Johan Commelin]

thanks for the pointer.

[Johan Commelin]

The mathlib bump is a really nice stress test for my new desktop. The fans are ramping up :grinning:

[Adam Topaz]

Johan Commelin said:

I mean this one: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/pseudoelements/near/278122957

I would have imagined that this would follow from the 5-lemma and the snake lemma without any additional fussing around with pseudoelements.

[Johan Commelin]

Seemed more annoying than I hoped.

[Adam Topaz]

It seems that we have all the ingredients needed for the proof -- we have that homology is a homological functor, so we get a LES associated to the triangle given by the cone, and we have the snake lemma which gives us the LES for homology coming from the SES. Now we just need to check that some diagram commutes to apply the 5-lemma (which we have in mathlib)

[Adam Topaz]

well, that proof would only work in the homotopy category since we need the API for homological functors, but that should be okay for our applications (I hope).

[Riccardo Brasca]

@Johan Commelin do you think your pseudoelement.biprod_ext is false in general?

[Johan Commelin]

maybe, I really don't know

[Riccardo Brasca]

Freyd–Mitchell seems to imply it, but maybe there is something subtle. Let me see if I can prove it.

[Adam Topaz]

Riccardo Brasca said:

Freyd–Mitchell seems to imply it, but maybe there is something subtle. Let me see if I can prove it.

IIRC pseudoelements are not how one constructs the Freyd-Mitchell embedding.

[Riccardo Brasca]

I have to a take a break, but Proposition 2.4.3 (vi) here immediately implies pseudoelement.biprod_ext if I am not misunderstanding anything.

[Riccardo Brasca]

I just realized that we have docs#category_theory.abelian.pseudoelement.pseudo_pullback, with a comment saying "Remark: Borceux claims that s is unique. I was unable to transform his proof sketch into a pen-and-paper proof of this fact, so naturally I was not able to formalize the proof."

[Riccardo Brasca]

And I am in the same situation

[Johan Commelin]

hmmz, so maybe it's hopeless to do this with pseudo-elements?

[Riccardo Brasca]

Now I am trying to understand the math-proof , we will see. It is an interesting question in its own

[Adam Topaz]

I pushed a start for the proof of the quasi iso result which uses the snake and 5 lemma (and no pseudoelements). Currently there is just a stub for the isomorphism of homologies in degree zero, and once that's done we would need to play with various shifts to get the actual result.

[Adam Topaz]

We do have a lemma called homotopy_category.is_quasi_iso_iff in for_mathlib/derived/lemmas.lean (I think?) which should be helpful with this shifting argument.

[Riccardo Brasca]

Concerning pseudoelements are essentially spent the last two hours trying to prove pseudoelement.biprod_ext by all the reasonable combinations of pullbakcs/products/... but at the end I arrive at the same goal as Johan, that I don't know how to prove (if it is true). I posted a question on mathoverflow.

[Riccardo Brasca]

My alarm clock is in four hours so I guess I have to stop playing with this :sweat_smile:

[Scott Morrison]

#13215 is ready for review/merge again. Thanks, @Adam Topaz for your suggestion re: simp lemmas.

[Scott Morrison]

Great, Johan just merged mathlib master, and I've now merged this branch back to lean-liquid/master.

[Scott Morrison]

I had a go at finishing extend in condensed/exact.lean, but things went pretty badly off the rails.

[Scott Morrison]

I'm not too certain what's going on, but at least the sorryd goals as currently stated have a problem because we are mixing up the has_limit and is_limit APIs in an awkward way.

[Scott Morrison]

I pushed a version that is all on the has_limit side. Hopefully it is just missing the right simp lemmas now??

[Johan Commelin]

I certainly hope so!

[Johan Commelin]

Thanks for your efforts!

[Scott Morrison]

No sorries in condensed/exact.lean! However for now I need -T200000. :-)

[Scott Morrison]

Just pushed.

[Scott Morrison]

Two associated PRs to mathlib: #13237 and #13238.

[Scott Morrison]

@Johan Commelin, the proof of extend_aux_1 should surely be improved. But I may defer to you for instructions as to whether I ought to improve it, or move on to something else. :-)

[Johan Commelin]

Wow, I'm really happy that this file is now done. Another green oval in the blueprint (I'll update it now).

[Johan Commelin]

If I were you I would just move on to something else. We can polish later.

[Johan Commelin]

@Scott Morrison Here's the updated blueprint: https://leanprover-community.github.io/liquid/dep_graph_section_2.html

[Johan Commelin]

For the record, the theta.bounded that is still blue should be ignored. Filippo has been working in that area, and once he's done we'll update the blueprint to reflect the correct proof.

[Johan Commelin]

@Filippo A. E. Nuccio If you already want to push an updated LaTeX proof, feel free to do so.

[Filippo A. E. Nuccio]

Yes, I am sorry, I have not been very active on the blueprint recently, but I will try to push an updated LaTeX proof soon.

[Riccardo Brasca]

I am afraid pseudoelement.biprod_ext is false.

I will wait a little bit to be sure I am not misunderstanding anything, but then I think I will modify the comment in docs#category_theory.abelian.pseudoelement.pseudo_pullback (CC @Markus Himmel ).

Without pseudoelement.biprod_ext I don't see how we can finish the current proof of cone.π_quasi_iso, so I guess @Adam Topaz approach is the right one, even if the final result is slightly weaker.

[Johan Commelin]

Thanks for sorting this out!

[Johan Commelin]

Adam and I are working on the other approach right now

[Adam Topaz]

@Johan Commelin I just proved this:

instance is_iso_Ext_flip_obj_map_of_is_quasi_iso [enough_projectives A] (i : ℤ)
  (X X' Y : 𝒦)
  (f : X ⟶ X') [homotopy_category.is_quasi_iso f] :
  is_iso (((Ext i).flip.obj Y).map f.op) :=

This should help us along with the LES without worrying too much about the derived cat.

[Adam Topaz]

This Ext is the bounded_homotopy_category.Ext..

[Adam Topaz]

We can do something similar in the second variable as well, if needed..

[Adam Topaz]

Getting there:

def Ext_five_term_exact_seq
  (n : ℤ)
  [enough_projectives A]
  (W : bounded_homotopy_category A)
  [homotopy_category.is_bounded_above ((homotopy_category.quotient _ _).obj X)]
  [homotopy_category.is_bounded_above ((homotopy_category.quotient _ _).obj Y)]
  [homotopy_category.is_bounded_above ((homotopy_category.quotient _ _).obj Z)]
  (w : ∀ i, short_exact (f.f i) (g.f i)) :
  let E := ((Ext n).flip.obj W).right_op in
  exact_seq Abᵒᵖ $
    [ arrow.mk (E.map (of_hom f))
    , E.map (of_hom g)
    , connecting_hom' f g n W w
    , E.map (-(of_hom f)⟦(1 : ℤ)⟧')] :=

[Adam Topaz]

Now we just need some shifting nonsense.

[Adam Topaz]

There is one sorry here about checking that some square commutes, in case anyone has the time:
https://github.com/leanprover-community/lean-liquid/blob/47262fc71f999823fe3a399d6ad1f9b0570039e7/src/for_mathlib/derived/les2.lean#L94

[Johan Commelin]

Who would have thought that getting a workable version of LES would have been so tricky.

[Riccardo Brasca]

Since this is claimed in well known reference, I wanted to really check that pseudoelement.biprod_ext is false. #13387

[Kevin Buzzard]

Johan Commelin said:

Who would have thought that getting a workable version of LES would have been so tricky.

Did people working in other theorem provers find this? I remember Hales once pointing out to me that "category theory in Coq seems to work fine". However there's this phrase in the UK (which I very much doubt is used elsewhere) -- "the proof of the pudding is in the eating", which means that it's one thing just to define something which you claim is a long exact sequence, and it's quite another thing to prove that it works by e.g. proving some fact about ext groups vanishing in some category of condensed abelian groups. Who are the people doing category theory in Coq? Furthermore, my memory of Unimath was that there was an absolute ton of category theory in it. Did they do long exact sequences?

OK so maybe this is a good question for the proof assistants stack exchange: I've asked it there.